support line context with depth;
basic setup for "isabelle" fold handling;
misc tuning;

--- a/src/Pure/Isar/outer_syntax.scala	Thu Oct 16 10:59:43 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Oct 16 12:09:57 2014 +0200
@@ -134,7 +134,8 @@
     }
   }
 
-  def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
+  def scan_line(input: CharSequence, context: Scan.Line_Context, depth: Int)
+    : (List[Token], Scan.Line_Context, Int) =
   {
     var in: Reader[Char] = new CharSequenceReader(input)
     val toks = new mutable.ListBuffer[Token]
@@ -146,7 +147,9 @@
           error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
       }
     }
-    (toks.toList, ctxt)
+
+    val depth1 = depth // FIXME
+    (toks.toList, ctxt, depth1)
   }
 
 

--- a/src/Tools/jEdit/src/bibtex_jedit.scala	Thu Oct 16 10:59:43 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Thu Oct 16 12:09:57 2014 +0200
@@ -154,7 +154,7 @@
   private val context_rules = new ParserRuleSet("bibtex", "MAIN")
 
   private class Line_Context(context: Option[Bibtex.Line_Context])
-    extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context)
+    extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context, 0)
 
 
   /* token marker */

--- a/src/Tools/jEdit/src/fold_handling.scala	Thu Oct 16 10:59:43 2014 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala	Thu Oct 16 12:09:57 2014 +0200
@@ -16,6 +16,23 @@
 
 object Fold_Handling
 {
+  /* input: dynamic line context  */
+
+  class Fold_Handler extends FoldHandler("isabelle")
+  {
+    override def equals(other: Any): Boolean =
+      other match {
+        case that: Fold_Handler => true
+        case _ => false
+      }
+
+    override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
+      Token_Markup.buffer_line_depth(buffer, line)
+  }
+
+
+  /* output: static document rendering */
+
   class Document_Fold_Handler(private val rendering: Rendering)
     extends FoldHandler("isabelle-document")
   {

--- a/src/Tools/jEdit/src/services.xml	Thu Oct 16 10:59:43 2014 +0200
+++ b/src/Tools/jEdit/src/services.xml	Thu Oct 16 12:09:57 2014 +0200
@@ -2,12 +2,15 @@
 <!DOCTYPE SERVICES SYSTEM "services.dtd">
 
 <SERVICES>
+  <SERVICE CLASS="org.gjt.sp.jedit.buffer.FoldHandler" NAME="isabelle">
+    new isabelle.jedit.Fold_Handling.Fold_Handler();
+  </SERVICE>
   <SERVICE CLASS="org.gjt.sp.jedit.gui.DynamicContextMenuService" NAME="Spell_Checker">
     new isabelle.jedit.Context_Menu();
   </SERVICE>
-	<SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
-		new isabelle.jedit.PIDE_Docking_Framework();
-	</SERVICE>
+  <SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
+    new isabelle.jedit.PIDE_Docking_Framework();
+  </SERVICE>
   <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
     new isabelle.jedit.Isabelle_Encoding();
   </SERVICE>

--- a/src/Tools/jEdit/src/token_markup.scala	Thu Oct 16 10:59:43 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Thu Oct 16 12:09:57 2014 +0200
@@ -175,13 +175,17 @@
 
   /* line context */
 
-  class Generic_Line_Context[C](rules: ParserRuleSet, val context: Option[C])
+  class Generic_Line_Context[C](
+      rules: ParserRuleSet,
+      val context: Option[C],
+      val depth: Int)
     extends TokenMarker.LineContext(rules, null)
   {
-    override def hashCode: Int = context.hashCode
+    override def hashCode: Int = (context, depth).hashCode
     override def equals(that: Any): Boolean =
       that match {
-        case other: Generic_Line_Context[_] => context == other.context
+        case other: Generic_Line_Context[_] =>
+          context == other.context && depth == other.depth
         case _ => false
       }
   }
@@ -190,58 +194,53 @@
     Untyped.get(buffer, "lineMgr") match {
       case line_mgr: LineManager =>
         line_mgr.getLineContext(line) match {
-          case ctxt: Generic_Line_Context[C] => Some(ctxt)
+          case c: Generic_Line_Context[C] => Some(c)
           case _ => None
         }
       case _ => None
     }
 
+  def buffer_line_depth(buffer: JEditBuffer, line: Int): Int =
+    buffer_line_context(buffer, line) match { case Some(c) => c.depth case None => 0 }
+
+
+  /* token marker */
 
   private val context_rules = new ParserRuleSet("isabelle", "MAIN")
 
-  private class Line_Context(context: Option[Scan.Line_Context])
-    extends Generic_Line_Context[Scan.Line_Context](context_rules, context)
-
-
-  /* token marker */
+  private class Line_Context(context: Option[Scan.Line_Context], depth: Int)
+    extends Generic_Line_Context[Scan.Line_Context](context_rules, context, depth)
 
   class Marker(mode: String) extends TokenMarker
   {
     override def markTokens(context: TokenMarker.LineContext,
         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
     {
-      val line_ctxt =
+      val (opt_ctxt, depth) =
         context match {
-          case c: Line_Context => c.context
-          case _ => Some(Scan.Finished)
+          case c: Line_Context => (c.context, c.depth)
+          case _ => (Some(Scan.Finished), 0)
         }
       val line = if (raw_line == null) new Segment else raw_line
 
       val context1 =
       {
-        def no_context =
-        {
-          val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
-          (List(styled_token), new Line_Context(None))
-        }
         val (styled_tokens, context1) =
-          if (mode == "isabelle-ml" || mode == "sml") {
-            if (line_ctxt.isDefined) {
-              val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, line_ctxt.get)
+          (opt_ctxt, Isabelle.mode_syntax(mode)) match {
+            case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
+              val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
               val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
-              (styled_tokens, new Line_Context(Some(ctxt1)))
-            }
-            else no_context
-          }
-          else {
-            Isabelle.mode_syntax(mode) match {
-              case Some(syntax) if syntax.has_tokens && line_ctxt.isDefined =>
-                val (tokens, ctxt1) = syntax.scan_line(line, line_ctxt.get)
-                val styled_tokens =
-                  tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
-                (styled_tokens, new Line_Context(Some(ctxt1)))
-              case _ => no_context
-            }
+              (styled_tokens, new Line_Context(Some(ctxt1), depth))
+
+            case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
+              val (tokens, ctxt1, depth1) = syntax.scan_line(line, ctxt, depth)
+              val styled_tokens =
+                tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
+              (styled_tokens, new Line_Context(Some(ctxt1), depth1))
+
+            case _ =>
+              val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
+              (List(styled_token), new Line_Context(None, 0))
           }
 
         val extended = extended_styles(line)
@@ -267,6 +266,7 @@
         handler.handleToken(line, JEditToken.END, line.count, 0, context1)
         context1
       }
+
       val context2 = context1.intern
       handler.setLineContext(context2)
       context2