some convenience actions/shortcuts for control symbols;
authorwenzelm
Wed Aug 17 16:01:27 2011 +0200 (2011-08-17)
changeset 4423836120feb70ed
parent 44237 2a2040c9d898
child 44239 47ecd30e018d
some convenience actions/shortcuts for control symbols;
src/Pure/General/symbol.scala
src/Pure/Thy/html.scala
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/General/symbol.scala	Wed Aug 17 15:14:48 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Wed Aug 17 16:01:27 2011 +0200
     1.3 @@ -356,14 +356,15 @@
     1.4      val ctrl_decoded: Set[Symbol] =
     1.5        Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
     1.6  
     1.7 -    val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
     1.8 -    val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
     1.9 -
    1.10 -    val bold_decoded = decode("\\<^bold>")
    1.11 +    val sub_decoded = decode("\\<^sub>")
    1.12 +    val sup_decoded = decode("\\<^sup>")
    1.13 +    val isub_decoded = decode("\\<^isub>")
    1.14 +    val isup_decoded = decode("\\<^isup>")
    1.15      val bsub_decoded = decode("\\<^bsub>")
    1.16      val esub_decoded = decode("\\<^esub>")
    1.17      val bsup_decoded = decode("\\<^bsup>")
    1.18      val esup_decoded = decode("\\<^esup>")
    1.19 +    val bold_decoded = decode("\\<^bold>")
    1.20    }
    1.21  
    1.22  
    1.23 @@ -401,11 +402,13 @@
    1.24    def is_controllable(sym: Symbol): Boolean =
    1.25      !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
    1.26  
    1.27 -  def is_subscript_decoded(sym: Symbol): Boolean = symbols.subscript_decoded.contains(sym)
    1.28 -  def is_superscript_decoded(sym: Symbol): Boolean = symbols.superscript_decoded.contains(sym)
    1.29 -  def is_bold_decoded(sym: Symbol): Boolean = sym == symbols.bold_decoded
    1.30 -  def is_bsub_decoded(sym: Symbol): Boolean = sym == symbols.bsub_decoded
    1.31 -  def is_esub_decoded(sym: Symbol): Boolean = sym == symbols.esub_decoded
    1.32 -  def is_bsup_decoded(sym: Symbol): Boolean = sym == symbols.bsup_decoded
    1.33 -  def is_esup_decoded(sym: Symbol): Boolean = sym == symbols.esup_decoded
    1.34 +  def sub_decoded: Symbol = symbols.sub_decoded
    1.35 +  def sup_decoded: Symbol = symbols.sup_decoded
    1.36 +  def isub_decoded: Symbol = symbols.isub_decoded
    1.37 +  def isup_decoded: Symbol = symbols.isup_decoded
    1.38 +  def bsub_decoded: Symbol = symbols.bsub_decoded
    1.39 +  def esub_decoded: Symbol = symbols.esub_decoded
    1.40 +  def bsup_decoded: Symbol = symbols.bsup_decoded
    1.41 +  def esup_decoded: Symbol = symbols.esup_decoded
    1.42 +  def bold_decoded: Symbol = symbols.bold_decoded
    1.43  }
     2.1 --- a/src/Pure/Thy/html.scala	Wed Aug 17 15:14:48 2011 +0200
     2.2 +++ b/src/Pure/Thy/html.scala	Wed Aug 17 16:01:27 2011 +0200
     2.3 @@ -83,13 +83,15 @@
     2.4              val s1 = syms.next
     2.5              def s2() = if (syms.hasNext) syms.next else ""
     2.6              if (s1 == "\n") add(XML.elem(BR))
     2.7 -            else if (Symbol.is_bsub_decoded(s1)) t ++= s1  // FIXME
     2.8 -            else if (Symbol.is_esub_decoded(s1)) t ++= s1  // FIXME
     2.9 -            else if (Symbol.is_bsup_decoded(s1)) t ++= s1  // FIXME
    2.10 -            else if (Symbol.is_esup_decoded(s1)) t ++= s1  // FIXME
    2.11 -            else if (Symbol.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    2.12 -            else if (Symbol.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    2.13 -            else if (Symbol.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
    2.14 +            else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)
    2.15 +              { add(hidden(s1)); add(sub(s2())) }
    2.16 +            else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)
    2.17 +              { add(hidden(s1)); add(sup(s2())) }
    2.18 +            else if (s1 == Symbol.bsub_decoded) t ++= s1  // FIXME
    2.19 +            else if (s1 == Symbol.esub_decoded) t ++= s1  // FIXME
    2.20 +            else if (s1 == Symbol.bsup_decoded) t ++= s1  // FIXME
    2.21 +            else if (s1 == Symbol.esup_decoded) t ++= s1  // FIXME
    2.22 +            else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
    2.23              else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
    2.24              else t ++= s1
    2.25            }
     3.1 --- a/src/Tools/jEdit/src/Isabelle.props	Wed Aug 17 15:14:48 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Wed Aug 17 16:01:27 2011 +0200
     3.3 @@ -37,6 +37,11 @@
     3.4  options.isabelle.auto-start.title=Auto Start
     3.5  options.isabelle.auto-start=true
     3.6  
     3.7 +#actions
     3.8 +isabelle.input-isub.shortcut=C+e DOWN
     3.9 +isabelle.input-isup.shortcut=C+e UP
    3.10 +isabelle.input-bold.shortcut=C+e RIGHT
    3.11 +
    3.12  #menu actions
    3.13  plugin.isabelle.jedit.Plugin.menu.label=Isabelle
    3.14  plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel
     4.1 --- a/src/Tools/jEdit/src/actions.xml	Wed Aug 17 15:14:48 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/actions.xml	Wed Aug 17 16:01:27 2011 +0200
     4.3 @@ -22,4 +22,40 @@
     4.4  			wm.addDockableWindow("isabelle-protocol");
     4.5  		</CODE>
     4.6  	</ACTION>
     4.7 +	<ACTION NAME="isabelle.input-sub">
     4.8 +	  <CODE>
     4.9 +	    isabelle.jedit.Isabelle.input_sub(textArea);
    4.10 +	  </CODE>
    4.11 +	</ACTION>
    4.12 +	<ACTION NAME="isabelle.input-sup">
    4.13 +	  <CODE>
    4.14 +	    isabelle.jedit.Isabelle.input_sup(textArea);
    4.15 +	  </CODE>
    4.16 +	</ACTION>
    4.17 +	<ACTION NAME="isabelle.input-isub">
    4.18 +	  <CODE>
    4.19 +	    isabelle.jedit.Isabelle.input_isub(textArea);
    4.20 +	  </CODE>
    4.21 +	</ACTION>
    4.22 +	<ACTION NAME="isabelle.input-isup">
    4.23 +	  <CODE>
    4.24 +	    isabelle.jedit.Isabelle.input_isup(textArea);
    4.25 +	  </CODE>
    4.26 +	</ACTION>
    4.27 +	<ACTION NAME="isabelle.input-bsub">
    4.28 +	  <CODE>
    4.29 +	    isabelle.jedit.Isabelle.input_bsub(textArea);
    4.30 +	  </CODE>
    4.31 +	</ACTION>
    4.32 +	<ACTION NAME="isabelle.input-bsup">
    4.33 +	  <CODE>
    4.34 +	    isabelle.jedit.Isabelle.input_bsup(textArea);
    4.35 +	  </CODE>
    4.36 +	</ACTION>
    4.37 +	<ACTION NAME="isabelle.input-bold">
    4.38 +	  <CODE>
    4.39 +	    isabelle.jedit.Isabelle.input_bold(textArea);
    4.40 +	  </CODE>
    4.41 +	</ACTION>
    4.42 +
    4.43  </ACTIONS>
    4.44 \ No newline at end of file
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 17 15:14:48 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 17 16:01:27 2011 +0200
     5.3 @@ -316,6 +316,24 @@
     5.4      }
     5.5      session.start(timeout, modes ::: List(logic))
     5.6    }
     5.7 +
     5.8 +
     5.9 +  /* convenience actions */
    5.10 +
    5.11 +  private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
    5.12 +  {
    5.13 +    s1.foreach(text_area.userInput(_))
    5.14 +    s2.foreach(text_area.userInput(_))
    5.15 +    s2.foreach(_ => text_area.goToPrevCharacter(false))
    5.16 +  }
    5.17 +
    5.18 +  def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded)
    5.19 +  def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded)
    5.20 +  def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded)
    5.21 +  def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded)
    5.22 +  def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
    5.23 +  def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
    5.24 +  def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
    5.25  }
    5.26  
    5.27  
     6.1 --- a/src/Tools/jEdit/src/token_markup.scala	Wed Aug 17 15:14:48 2011 +0200
     6.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Wed Aug 17 16:01:27 2011 +0200
     6.3 @@ -107,11 +107,11 @@
     6.4  
     6.5    def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
     6.6    {
     6.7 -    // FIXME Symbol.is_bsub_decoded etc.
     6.8 +    // FIXME Symbol.bsub_decoded etc.
     6.9      def ctrl_style(sym: String): Option[Byte => Byte] =
    6.10 -      if (Symbol.is_subscript_decoded(sym)) Some(subscript(_))
    6.11 -      else if (Symbol.is_superscript_decoded(sym)) Some(superscript(_))
    6.12 -      else if (Symbol.is_bold_decoded(sym)) Some(bold(_))
    6.13 +      if (sym == Symbol.sub_decoded || sym == Symbol.isub_decoded) Some(subscript(_))
    6.14 +      else if (sym == Symbol.sup_decoded || sym == Symbol.isup_decoded) Some(superscript(_))
    6.15 +      else if (sym == Symbol.bold_decoded) Some(bold(_))
    6.16        else None
    6.17  
    6.18      var result = Map[Text.Offset, Byte => Byte]()