# HG changeset patch
# User wenzelm
# Date 1445265465 -7200
# Node ID 07c8d5d8acab4d348e656633a54bffcf1de1ce3f
# Parent  391814730b40d36ed67bfb5c354d74552fb32e1e
added action "isabelle-emph";
changed shortcut of action "isabelle-reset";

diff -r 391814730b40 -r 07c8d5d8acab NEWS
--- 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 ***
 
diff -r 391814730b40 -r 07c8d5d8acab src/Doc/JEdit/JEdit.thy
--- 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>
diff -r 391814730b40 -r 07c8d5d8acab src/Pure/General/symbol.scala
--- 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
 }
diff -r 391814730b40 -r 07c8d5d8acab src/Tools/jEdit/src/actions.xml
--- 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);
diff -r 391814730b40 -r 07c8d5d8acab src/Tools/jEdit/src/isabelle.scala
--- 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, "") }
 
diff -r 391814730b40 -r 07c8d5d8acab src/Tools/jEdit/src/jEdit.props
--- 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