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]()