# HG changeset patch
# User immler@in.tum.de
# Date 1231691756 -3600
# Node ID c7d7a92fe3d55f465d89cefa54960d940e4fb235
# Parent  191a481f0594b8a0c13bd15242a1b618e37b58a6
created DynamicTokenMarker
included it in ProverSetup and registered at prover

diff -r 191a481f0594 -r c7d7a92fe3d5 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sun Jan 11 17:35:56 2009 +0100
@@ -0,0 +1,40 @@
+/*
+ * include isabelle's command- and keyword-declarations
+ * live in jEdits syntax-highlighting
+ * 
+ * one TokenMarker per prover
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+import org.gjt.sp.jedit.syntax.{ModeProvider, Token, TokenMarker, ParserRuleSet, KeywordMap}
+
+class DynamicTokenMarker extends TokenMarker {
+
+  val ruleset = new ParserRuleSet("isabelle", "MAIN")
+
+  // copy rules and keywords from basic isabelle mode
+  val original = ModeProvider.instance.getMode("isabelle").getTokenMarker.getMainRuleSet
+  ruleset.addRuleSet(original)
+  ruleset.setKeywords(new KeywordMap(false))
+  ruleset.setDefault(0)
+  ruleset.setDigitRegexp(null)
+  ruleset.setEscapeRule(original.getEscapeRule)
+  ruleset.setHighlightDigits(false)
+  ruleset.setIgnoreCase(false)
+  ruleset.setNoWordSep("_")
+  ruleset.setProperties(null)
+  ruleset.setTerminateChar(-1)
+
+  addRuleSet(ruleset)
+
+  def += (token:String, kind:String) = {
+    val kind_byte = kind match {
+      case Markup.COMMAND => Token.KEYWORD4
+      case Markup.KEYWORD => Token.KEYWORD3
+    }
+    getMainRuleSet.getKeywords.add(token, kind_byte)
+  }
+}
diff -r 191a481f0594 -r c7d7a92fe3d5 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Sun Jan 11 13:46:26 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Sun Jan 11 17:35:56 2009 +0100
@@ -42,6 +42,8 @@
     prover.set_document(theory_view,
         if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir)
     theory_view.activate
+
+    //register output-view
     prover.output_info += (text =>
       {
         output_text_view.append(text)
@@ -70,10 +72,18 @@
           state_panel.setDocument(state.results_xml, UserAgent.baseURL)
       }
     })
+  
+    // one independent token marker per prover
+    val token_marker = new DynamicTokenMarker
+    buffer.setTokenMarker(token_marker)
+
+    // register for new declarations
+    prover.decl_info += (pair => pair match {case (a,b) => token_marker += (a,b)})
 
   }
 
   def deactivate {
+    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
     theory_view.deactivate
     prover.stop
   }