--- a/NEWS Mon Oct 19 16:26:01 2015 +0200
+++ b/NEWS Mon Oct 19 16:37:45 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 16:26:01 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy Mon Oct 19 16:37:45 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/symbol.scala Mon Oct 19 16:26:01 2015 +0200
+++ b/src/Pure/General/symbol.scala Mon Oct 19 16:37:45 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/Tools/jEdit/src/actions.xml Mon Oct 19 16:26:01 2015 +0200
+++ b/src/Tools/jEdit/src/actions.xml Mon Oct 19 16:37:45 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 16:26:01 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Oct 19 16:37:45 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 16:26:01 2015 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Mon Oct 19 16:37:45 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