# HG changeset patch
# User wenzelm
# Date 1313589687 -7200
# Node ID 36120feb70edf7cbf6e0feb0ca17a00c535cbd10
# Parent 2a2040c9d89803073661871aabe6cd845a58c7d5
some convenience actions/shortcuts for control symbols;
diff -r 2a2040c9d898 -r 36120feb70ed src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Pure/General/symbol.scala Wed Aug 17 16:01:27 2011 +0200
@@ -356,14 +356,15 @@
val ctrl_decoded: Set[Symbol] =
Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
- val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
- val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
-
- val bold_decoded = decode("\\<^bold>")
+ val sub_decoded = decode("\\<^sub>")
+ val sup_decoded = decode("\\<^sup>")
+ val isub_decoded = decode("\\<^isub>")
+ val isup_decoded = decode("\\<^isup>")
val bsub_decoded = decode("\\<^bsub>")
val esub_decoded = decode("\\<^esub>")
val bsup_decoded = decode("\\<^bsup>")
val esup_decoded = decode("\\<^esup>")
+ val bold_decoded = decode("\\<^bold>")
}
@@ -401,11 +402,13 @@
def is_controllable(sym: Symbol): Boolean =
!is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
- def is_subscript_decoded(sym: Symbol): Boolean = symbols.subscript_decoded.contains(sym)
- def is_superscript_decoded(sym: Symbol): Boolean = symbols.superscript_decoded.contains(sym)
- def is_bold_decoded(sym: Symbol): Boolean = sym == symbols.bold_decoded
- def is_bsub_decoded(sym: Symbol): Boolean = sym == symbols.bsub_decoded
- def is_esub_decoded(sym: Symbol): Boolean = sym == symbols.esub_decoded
- def is_bsup_decoded(sym: Symbol): Boolean = sym == symbols.bsup_decoded
- def is_esup_decoded(sym: Symbol): Boolean = sym == symbols.esup_decoded
+ def sub_decoded: Symbol = symbols.sub_decoded
+ def sup_decoded: Symbol = symbols.sup_decoded
+ def isub_decoded: Symbol = symbols.isub_decoded
+ def isup_decoded: Symbol = symbols.isup_decoded
+ def bsub_decoded: Symbol = symbols.bsub_decoded
+ def esub_decoded: Symbol = symbols.esub_decoded
+ def bsup_decoded: Symbol = symbols.bsup_decoded
+ def esup_decoded: Symbol = symbols.esup_decoded
+ def bold_decoded: Symbol = symbols.bold_decoded
}
diff -r 2a2040c9d898 -r 36120feb70ed src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Pure/Thy/html.scala Wed Aug 17 16:01:27 2011 +0200
@@ -83,13 +83,15 @@
val s1 = syms.next
def s2() = if (syms.hasNext) syms.next else ""
if (s1 == "\n") add(XML.elem(BR))
- else if (Symbol.is_bsub_decoded(s1)) t ++= s1 // FIXME
- else if (Symbol.is_esub_decoded(s1)) t ++= s1 // FIXME
- else if (Symbol.is_bsup_decoded(s1)) t ++= s1 // FIXME
- else if (Symbol.is_esup_decoded(s1)) t ++= s1 // FIXME
- else if (Symbol.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
- else if (Symbol.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
- else if (Symbol.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
+ else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)
+ { add(hidden(s1)); add(sub(s2())) }
+ else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)
+ { add(hidden(s1)); add(sup(s2())) }
+ else if (s1 == Symbol.bsub_decoded) t ++= s1 // FIXME
+ else if (s1 == Symbol.esub_decoded) t ++= s1 // FIXME
+ else if (s1 == Symbol.bsup_decoded) t ++= s1 // FIXME
+ else if (s1 == Symbol.esup_decoded) t ++= s1 // FIXME
+ else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
else t ++= s1
}
diff -r 2a2040c9d898 -r 36120feb70ed src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Wed Aug 17 16:01:27 2011 +0200
@@ -37,6 +37,11 @@
options.isabelle.auto-start.title=Auto Start
options.isabelle.auto-start=true
+#actions
+isabelle.input-isub.shortcut=C+e DOWN
+isabelle.input-isup.shortcut=C+e UP
+isabelle.input-bold.shortcut=C+e RIGHT
+
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel
diff -r 2a2040c9d898 -r 36120feb70ed src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Tools/jEdit/src/actions.xml Wed Aug 17 16:01:27 2011 +0200
@@ -22,4 +22,40 @@
wm.addDockableWindow("isabelle-protocol");
+
+
+ isabelle.jedit.Isabelle.input_sub(textArea);
+
+
+
+
+ isabelle.jedit.Isabelle.input_sup(textArea);
+
+
+
+
+ isabelle.jedit.Isabelle.input_isub(textArea);
+
+
+
+
+ isabelle.jedit.Isabelle.input_isup(textArea);
+
+
+
+
+ isabelle.jedit.Isabelle.input_bsub(textArea);
+
+
+
+
+ isabelle.jedit.Isabelle.input_bsup(textArea);
+
+
+
+
+ isabelle.jedit.Isabelle.input_bold(textArea);
+
+
+
\ No newline at end of file
diff -r 2a2040c9d898 -r 36120feb70ed src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Aug 17 16:01:27 2011 +0200
@@ -316,6 +316,24 @@
}
session.start(timeout, modes ::: List(logic))
}
+
+
+ /* convenience actions */
+
+ private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
+ {
+ s1.foreach(text_area.userInput(_))
+ s2.foreach(text_area.userInput(_))
+ s2.foreach(_ => text_area.goToPrevCharacter(false))
+ }
+
+ def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded)
+ def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded)
+ def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded)
+ def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded)
+ def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
+ def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
+ def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
}
diff -r 2a2040c9d898 -r 36120feb70ed src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala Wed Aug 17 15:14:48 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Wed Aug 17 16:01:27 2011 +0200
@@ -107,11 +107,11 @@
def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
{
- // FIXME Symbol.is_bsub_decoded etc.
+ // FIXME Symbol.bsub_decoded etc.
def ctrl_style(sym: String): Option[Byte => Byte] =
- if (Symbol.is_subscript_decoded(sym)) Some(subscript(_))
- else if (Symbol.is_superscript_decoded(sym)) Some(superscript(_))
- else if (Symbol.is_bold_decoded(sym)) Some(bold(_))
+ if (sym == Symbol.sub_decoded || sym == Symbol.isub_decoded) Some(subscript(_))
+ else if (sym == Symbol.sup_decoded || sym == Symbol.isup_decoded) Some(superscript(_))
+ else if (sym == Symbol.bold_decoded) Some(bold(_))
else None
var result = Map[Text.Offset, Byte => Byte]()