# HG changeset patch # User wenzelm # Date 1445267993 -7200 # Node ID 0cc8016cc1959860cb1d7a497b4a8baa6a46f088 # Parent 3885464e4874eba18790d2e4aa26857aba343072# Parent dcc8e1d34b189955e757b3b1f710eb88a0166e43 merged diff -r 3885464e4874 -r 0cc8016cc195 NEWS --- a/NEWS Mon Oct 19 15:58:13 2015 +0200 +++ b/NEWS Mon Oct 19 17:19:53 2015 +0200 @@ -53,6 +53,13 @@ state output in the Output panel: suppressing this reduces resource requirements of prover time and GUI space. +* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls +emphasized text style; the effect is visible in document output, not in +the editor. + +* Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE, +instead of former C+e LEFT. + *** Document preparation *** diff -r 3885464e4874 -r 0cc8016cc195 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Mon Oct 19 15:58:13 2015 +0200 +++ b/src/Doc/JEdit/JEdit.thy Mon Oct 19 17:19:53 2015 +0200 @@ -579,13 +579,19 @@ superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{action_ref "isabelle.control-sup"} \\ subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{action_ref "isabelle.control-sub"} \\ bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{action_ref "isabelle.control-bold"} \\ - reset & & @{verbatim "C+e LEFT"} & @{action_ref "isabelle.control-reset"} \\ + emphasized & @{verbatim "\<^emph>"} & @{verbatim "C+e LEF"} & @{action_ref "isabelle.control-emph"} \\ + reset & & @{verbatim "C+e BACK_SPACE"} & @{action_ref "isabelle.control-reset"} \\ \end{tabular} \<^medskip> - - To produce a single control symbol, it is also possible to complete - on @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub}, - @{verbatim "\\"}@{verbatim bold} as for regular symbols.\ + + To produce a single control symbol, it is also possible to complete on + @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub}, @{verbatim + "\\"}@{verbatim bold}, @{verbatim "\\"}@{verbatim emph} as for regular + symbols. + + The emphasized style only takes effect in document output, not in the + editor. +\ section \SideKick parsers \label{sec:sidekick}\ diff -r 3885464e4874 -r 0cc8016cc195 src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Mon Oct 19 15:58:13 2015 +0200 +++ b/src/Pure/General/antiquote.ML Mon Oct 19 17:19:53 2015 +0200 @@ -84,15 +84,15 @@ val scan_antiq_body = Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || - Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 || + Symbol_Pos.scan_cartouche err_prefix || Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single; in val scan_control = Scan.one (Symbol.is_control o Symbol_Pos.symbol) -- - Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> - (fn ((control, pos), (_, body)) => + Symbol_Pos.scan_cartouche err_prefix >> + (fn ((control, pos), body) => let val Symbol.Control name = Symbol.decode control; val range = Symbol_Pos.range ((control, pos) :: body); @@ -109,7 +109,7 @@ body = body}); val scan_antiquote = - scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text; + scan_txt >> Text || scan_control >> Control || scan_antiq >> Antiq; end; diff -r 3885464e4874 -r 0cc8016cc195 src/Pure/General/antiquote.scala --- a/src/Pure/General/antiquote.scala Mon Oct 19 15:58:13 2015 +0200 +++ b/src/Pure/General/antiquote.scala Mon Oct 19 17:19:53 2015 +0200 @@ -42,7 +42,7 @@ "@{" ~ rep(antiq_body) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z } val antiquote: Parser[Antiquote] = - control ^^ (x => Control(x)) | (antiq ^^ (x => Antiq(x)) | txt ^^ (x => Text(x))) + txt ^^ (x => Text(x)) | (control ^^ (x => Control(x)) | antiq ^^ (x => Antiq(x))) } diff -r 3885464e4874 -r 0cc8016cc195 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Mon Oct 19 15:58:13 2015 +0200 +++ b/src/Pure/General/symbol.scala Mon Oct 19 17:19:53 2015 +0200 @@ -451,6 +451,7 @@ val bsup_decoded = decode("\\<^bsup>") val esup_decoded = decode("\\<^esup>") val bold_decoded = decode("\\<^bold>") + val emph_decoded = decode("\\<^emph>") } @@ -533,4 +534,5 @@ def bsup_decoded: Symbol = symbols.bsup_decoded def esup_decoded: Symbol = symbols.esup_decoded def bold_decoded: Symbol = symbols.bold_decoded + def emph_decoded: Symbol = symbols.emph_decoded } diff -r 3885464e4874 -r 0cc8016cc195 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Mon Oct 19 15:58:13 2015 +0200 +++ b/src/Pure/ML/ml_lex.ML Mon Oct 19 17:19:53 2015 +0200 @@ -328,10 +328,11 @@ |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan)) (fn msg => recover msg >> map Antiquote.Text)) - |> Source.exhaust - |> tap (Position.reports o Antiquote.antiq_reports) - |> tap (Position.reports_text o maps (fn Antiquote.Text t => [token_report SML t] | _ => [])) - |> tap (List.app check); + |> Source.exhaust; + val _ = Position.reports (Antiquote.antiq_reports input); + val _ = + Position.reports_text (maps (fn Antiquote.Text t => [token_report SML t] | _ => []) input); + val _ = List.app check input; in input @ termination end; in diff -r 3885464e4874 -r 0cc8016cc195 src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Mon Oct 19 15:58:13 2015 +0200 +++ b/src/Pure/Thy/present.scala Mon Oct 19 17:19:53 2015 +0200 @@ -103,7 +103,7 @@ if (info.options.bool("browser_info")) { Isabelle_System.mkdirs(session_prefix) - File.copy(graph_file, (session_prefix + Path.basic("session_graph.pdf")).file) + File.write(session_prefix + Path.basic("session_graph.pdf"), File.read(graph_file)) File.copy(Path.explode("~~/etc/isabelle.css"), session_prefix) File.copy(Path.explode("~~/lib/fonts/IsabelleText.ttf"), session_prefix) File.copy(Path.explode("~~/lib/fonts/IsabelleTextBold.ttf"), session_prefix) diff -r 3885464e4874 -r 0cc8016cc195 src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Mon Oct 19 15:58:13 2015 +0200 +++ b/src/Tools/jEdit/src/actions.xml Mon Oct 19 17:19:53 2015 +0200 @@ -87,6 +87,11 @@ isabelle.jedit.Isabelle.control_bold(textArea); + + + isabelle.jedit.Isabelle.control_emph(textArea); + + isabelle.jedit.Isabelle.control_reset(textArea); diff -r 3885464e4874 -r 0cc8016cc195 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Mon Oct 19 15:58:13 2015 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Mon Oct 19 17:19:53 2015 +0200 @@ -312,6 +312,9 @@ def control_bold(text_area: JEditTextArea) { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) } + def control_emph(text_area: JEditTextArea) + { Token_Markup.edit_control_style(text_area, Symbol.emph_decoded) } + def control_reset(text_area: JEditTextArea) { Token_Markup.edit_control_style(text_area, "") } diff -r 3885464e4874 -r 0cc8016cc195 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Mon Oct 19 15:58:13 2015 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Mon Oct 19 17:19:53 2015 +0200 @@ -201,8 +201,10 @@ isabelle.complete.shortcut2=C+b isabelle.control-bold.label=Control bold isabelle.control-bold.shortcut=C+e RIGHT +isabelle.control-emph.label=Control emphasized +isabelle.control-emph.shortcut=C+e LEFT isabelle.control-reset.label=Control reset -isabelle.control-reset.shortcut=C+e LEFT +isabelle.control-reset.shortcut=C+e BACK_SPACE isabelle.control-sub.label=Control subscript isabelle.control-sub.shortcut=C+e DOWN isabelle.control-sup.label=Control superscript