--- 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 ***
--- 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.\<close>
+
+ 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.
+\<close>
section \<open>SideKick parsers \label{sec:sidekick}\<close>
--- 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;
--- 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)))
}
--- 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
}
--- 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
--- 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)
--- 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);
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.control-emph">
+ <CODE>
+ isabelle.jedit.Isabelle.control_emph(textArea);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.control-reset">
<CODE>
isabelle.jedit.Isabelle.control_reset(textArea);
--- 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, "") }
--- 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