# HG changeset patch
# User wenzelm
# Date 1417452667 -3600
# Node ID 9f87eb298b755bf18fdf48eeb333202fc4d8ef29
# Parent  7836d927ffca8fe5ec93efb7d902b6a2f3b02ed4
Sidekick syntax is derived from buffer (and its mode), instead of parser name;

diff -r 7836d927ffca -r 9f87eb298b75 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Dec 01 17:43:23 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Dec 01 17:51:07 2014 +0100
@@ -30,7 +30,6 @@
     List(
       "isabelle",         // theory source
       "isabelle-ml",      // ML source
-      "isabelle-markup",  // SideKick markup tree
       "isabelle-news",    // NEWS
       "isabelle-options", // etc/options
       "isabelle-output",  // pretty text area output
@@ -56,7 +55,7 @@
 
   def mode_syntax(name: String): Option[Outer_Syntax] =
     name match {
-      case "isabelle" | "isabelle-markup" => session_syntax()
+      case "isabelle" => session_syntax()
       case "isabelle-options" => Some(Options.options_syntax)
       case "isabelle-root" => Some(Build.root_syntax)
       case "isabelle-ml" => Some(ml_syntax)
diff -r 7836d927ffca -r 9f87eb298b75 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Dec 01 17:43:23 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Dec 01 17:51:07 2014 +0100
@@ -83,7 +83,7 @@
 
     // FIXME lock buffer (!??)
     val data = Isabelle_Sidekick.root_data(buffer)
-    val syntax = Isabelle.mode_syntax(name)
+    val syntax = Isabelle.buffer_syntax(buffer)
     val ok =
       if (syntax.isDefined) {
         val ok = parser(buffer, syntax.get, data)