# HG changeset patch
# User wenzelm
# Date 1489582179 -3600
# Node ID 41d12227d5dc927e50d8514468873bf5b5e1fae9
# Parent  a0701669d159c253361581fc945fc919143b2c0a
clarified modules;

diff -r a0701669d159 -r 41d12227d5dc src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Mar 15 13:35:14 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Mar 15 13:49:39 2017 +0100
@@ -379,19 +379,19 @@
   /* control styles */
 
   def control_sub(text_area: JEditTextArea)
-  { Token_Markup.edit_control_style(text_area, Symbol.sub) }
+  { Syntax_Style.edit_control_style(text_area, Symbol.sub) }
 
   def control_sup(text_area: JEditTextArea)
-  { Token_Markup.edit_control_style(text_area, Symbol.sup) }
+  { Syntax_Style.edit_control_style(text_area, Symbol.sup) }
 
   def control_bold(text_area: JEditTextArea)
-  { Token_Markup.edit_control_style(text_area, Symbol.bold) }
+  { Syntax_Style.edit_control_style(text_area, Symbol.bold) }
 
   def control_emph(text_area: JEditTextArea)
-  { Token_Markup.edit_control_style(text_area, Symbol.emph) }
+  { Syntax_Style.edit_control_style(text_area, Symbol.emph) }
 
   def control_reset(text_area: JEditTextArea)
-  { Token_Markup.edit_control_style(text_area, "") }
+  { Syntax_Style.edit_control_style(text_area, "") }
 
 
   /* block styles */
diff -r a0701669d159 -r 41d12227d5dc src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Mar 15 13:35:14 2017 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Wed Mar 15 13:49:39 2017 +0100
@@ -97,7 +97,7 @@
       Action(Symbol.decode(symbol)) {
         val text_area = view.getTextArea
         if (is_control && HTML.control.isDefinedAt(symbol))
-          Token_Markup.edit_control_style(text_area, symbol)
+          Syntax_Style.edit_control_style(text_area, symbol)
         else
           text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
         text_area.requestFocus
@@ -111,7 +111,7 @@
   {
     action = Action("Reset") {
       val text_area = view.getTextArea
-      Token_Markup.edit_control_style(text_area, "")
+      Syntax_Style.edit_control_style(text_area, "")
       text_area.requestFocus
     }
     tooltip = "Reset control symbols within text"
diff -r a0701669d159 -r 41d12227d5dc src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Wed Mar 15 13:35:14 2017 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala	Wed Mar 15 13:49:39 2017 +0100
@@ -15,10 +15,13 @@
 
 import org.gjt.sp.util.SyntaxUtilities
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
+import org.gjt.sp.jedit.textarea.TextArea
 
 
 object Syntax_Style
 {
+  /* extended syntax styles */
+
   private val plain_range: Int = JEditToken.ID_COUNT
   private val full_range = 6 * plain_range + 1
   private def check_range(i: Int) { require(0 <= i && i < plain_range) }
@@ -120,4 +123,45 @@
     }
     result
   }
+
+
+  /* editing support for control symbols */
+
+  def edit_control_style(text_area: TextArea, control: String)
+  {
+    GUI_Thread.assert {}
+
+    val buffer = text_area.getBuffer
+
+    val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control)
+
+    def update_style(text: String): String =
+    {
+      val result = new StringBuilder
+      for (sym <- Symbol.iterator(text) if !HTML.control.isDefinedAt(sym)) {
+        if (Symbol.is_controllable(sym)) result ++= control_decoded
+        result ++= sym
+      }
+      result.toString
+    }
+
+    text_area.getSelection.foreach(sel => {
+      val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
+      JEdit_Lib.try_get_text(buffer, before) match {
+        case Some(s) if HTML.control.isDefinedAt(s) =>
+          text_area.extendSelection(before.start, before.stop)
+        case _ =>
+      }
+    })
+
+    text_area.getSelection.toList match {
+      case Nil =>
+        text_area.setSelectedText(control_decoded)
+      case sels =>
+        JEdit_Lib.buffer_edit(buffer) {
+          sels.foreach(sel =>
+            text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel))))
+        }
+    }
+  }
 }
diff -r a0701669d159 -r 41d12227d5dc src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Wed Mar 15 13:35:14 2017 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Wed Mar 15 13:49:39 2017 +0100
@@ -9,65 +9,19 @@
 
 import isabelle._
 
-import java.awt.{Font, Color}
-import java.awt.font.TextAttribute
-import java.awt.geom.AffineTransform
 import javax.swing.text.Segment
 
 import scala.collection.convert.WrapAsJava
 
-import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.jedit.{jEdit, Mode, Buffer}
+import org.gjt.sp.jedit.{Mode, Buffer}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
-  ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
+  ParserRuleSet, ModeProvider, XModeHandler}
 import org.gjt.sp.jedit.indent.IndentRule
-import org.gjt.sp.jedit.textarea.{TextArea, Selection}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 
 
 object Token_Markup
 {
-  /* editing support for control symbols */
-
-  def edit_control_style(text_area: TextArea, control: String)
-  {
-    GUI_Thread.assert {}
-
-    val buffer = text_area.getBuffer
-
-    val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control)
-
-    def update_style(text: String): String =
-    {
-      val result = new StringBuilder
-      for (sym <- Symbol.iterator(text) if !HTML.control.isDefinedAt(sym)) {
-        if (Symbol.is_controllable(sym)) result ++= control_decoded
-        result ++= sym
-      }
-      result.toString
-    }
-
-    text_area.getSelection.foreach(sel => {
-      val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
-      JEdit_Lib.try_get_text(buffer, before) match {
-        case Some(s) if HTML.control.isDefinedAt(s) =>
-          text_area.extendSelection(before.start, before.stop)
-        case _ =>
-      }
-    })
-
-    text_area.getSelection.toList match {
-      case Nil =>
-        text_area.setSelectedText(control_decoded)
-      case sels =>
-        JEdit_Lib.buffer_edit(buffer) {
-          sels.foreach(sel =>
-            text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel))))
-        }
-    }
-  }
-
-
   /* line context */
 
   object Line_Context