added action "isabelle-emph";
authorwenzelm
Mon Oct 19 16:37:45 2015 +0200 (2015-10-19)
changeset 6148307c8d5d8acab
parent 61482 391814730b40
child 61484 dcc8e1d34b18
added action "isabelle-emph";
changed shortcut of action "isabelle-reset";
NEWS
src/Doc/JEdit/JEdit.thy
src/Pure/General/symbol.scala
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/NEWS	Mon Oct 19 16:26:01 2015 +0200
     1.2 +++ b/NEWS	Mon Oct 19 16:37:45 2015 +0200
     1.3 @@ -53,6 +53,13 @@
     1.4  state output in the Output panel: suppressing this reduces resource
     1.5  requirements of prover time and GUI space.
     1.6  
     1.7 +* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls
     1.8 +emphasized text style; the effect is visible in document output, not in
     1.9 +the editor.
    1.10 +
    1.11 +* Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,
    1.12 +instead of former C+e LEFT.
    1.13 +
    1.14  
    1.15  *** Document preparation ***
    1.16  
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Mon Oct 19 16:26:01 2015 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon Oct 19 16:37:45 2015 +0200
     2.3 @@ -579,13 +579,19 @@
     2.4      superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{action_ref "isabelle.control-sup"} \\
     2.5      subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{action_ref "isabelle.control-sub"} \\
     2.6      bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{action_ref "isabelle.control-bold"} \\
     2.7 -    reset & & @{verbatim "C+e LEFT"} & @{action_ref "isabelle.control-reset"} \\
     2.8 +    emphasized & @{verbatim "\<^emph>"} & @{verbatim "C+e LEF"} & @{action_ref "isabelle.control-emph"} \\
     2.9 +    reset & & @{verbatim "C+e BACK_SPACE"} & @{action_ref "isabelle.control-reset"} \\
    2.10    \end{tabular}
    2.11    \<^medskip>
    2.12 - 
    2.13 -  To produce a single control symbol, it is also possible to complete
    2.14 -  on @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub},
    2.15 -  @{verbatim "\\"}@{verbatim bold} as for regular symbols.\<close>
    2.16 +
    2.17 +  To produce a single control symbol, it is also possible to complete on
    2.18 +  @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub}, @{verbatim
    2.19 +  "\\"}@{verbatim bold}, @{verbatim "\\"}@{verbatim emph} as for regular
    2.20 +  symbols.
    2.21 +
    2.22 +  The emphasized style only takes effect in document output, not in the
    2.23 +  editor.
    2.24 +\<close>
    2.25  
    2.26  
    2.27  section \<open>SideKick parsers \label{sec:sidekick}\<close>
     3.1 --- a/src/Pure/General/symbol.scala	Mon Oct 19 16:26:01 2015 +0200
     3.2 +++ b/src/Pure/General/symbol.scala	Mon Oct 19 16:37:45 2015 +0200
     3.3 @@ -451,6 +451,7 @@
     3.4      val bsup_decoded = decode("\\<^bsup>")
     3.5      val esup_decoded = decode("\\<^esup>")
     3.6      val bold_decoded = decode("\\<^bold>")
     3.7 +    val emph_decoded = decode("\\<^emph>")
     3.8    }
     3.9  
    3.10  
    3.11 @@ -533,4 +534,5 @@
    3.12    def bsup_decoded: Symbol = symbols.bsup_decoded
    3.13    def esup_decoded: Symbol = symbols.esup_decoded
    3.14    def bold_decoded: Symbol = symbols.bold_decoded
    3.15 +  def emph_decoded: Symbol = symbols.emph_decoded
    3.16  }
     4.1 --- a/src/Tools/jEdit/src/actions.xml	Mon Oct 19 16:26:01 2015 +0200
     4.2 +++ b/src/Tools/jEdit/src/actions.xml	Mon Oct 19 16:37:45 2015 +0200
     4.3 @@ -87,6 +87,11 @@
     4.4  	    isabelle.jedit.Isabelle.control_bold(textArea);
     4.5  	  </CODE>
     4.6  	</ACTION>
     4.7 +	<ACTION NAME="isabelle.control-emph">
     4.8 +	  <CODE>
     4.9 +	    isabelle.jedit.Isabelle.control_emph(textArea);
    4.10 +	  </CODE>
    4.11 +	</ACTION>
    4.12  	<ACTION NAME="isabelle.control-reset">
    4.13  	  <CODE>
    4.14  	    isabelle.jedit.Isabelle.control_reset(textArea);
     5.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Oct 19 16:26:01 2015 +0200
     5.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Oct 19 16:37:45 2015 +0200
     5.3 @@ -312,6 +312,9 @@
     5.4    def control_bold(text_area: JEditTextArea)
     5.5    { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
     5.6  
     5.7 +  def control_emph(text_area: JEditTextArea)
     5.8 +  { Token_Markup.edit_control_style(text_area, Symbol.emph_decoded) }
     5.9 +
    5.10    def control_reset(text_area: JEditTextArea)
    5.11    { Token_Markup.edit_control_style(text_area, "") }
    5.12  
     6.1 --- a/src/Tools/jEdit/src/jEdit.props	Mon Oct 19 16:26:01 2015 +0200
     6.2 +++ b/src/Tools/jEdit/src/jEdit.props	Mon Oct 19 16:37:45 2015 +0200
     6.3 @@ -201,8 +201,10 @@
     6.4  isabelle.complete.shortcut2=C+b
     6.5  isabelle.control-bold.label=Control bold
     6.6  isabelle.control-bold.shortcut=C+e RIGHT
     6.7 +isabelle.control-emph.label=Control emphasized
     6.8 +isabelle.control-emph.shortcut=C+e LEFT
     6.9  isabelle.control-reset.label=Control reset
    6.10 -isabelle.control-reset.shortcut=C+e LEFT
    6.11 +isabelle.control-reset.shortcut=C+e BACK_SPACE
    6.12  isabelle.control-sub.label=Control subscript
    6.13  isabelle.control-sub.shortcut=C+e DOWN
    6.14  isabelle.control-sup.label=Control superscript