# HG changeset patch
# User wenzelm
# Date 1289401515 -3600
# Node ID 34823a2cba08522458b5a8b2c540c7badaae92ad
# Parent  2269544b645730911fc7df8fe6db1df729a13cc4# Parent  b6feba6c9fccf99c951408b85ed30e7793a11836
merged

diff -r 2269544b6457 -r 34823a2cba08 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Nov 10 16:05:15 2010 +0100
@@ -552,9 +552,13 @@
 
 fun status e =
   let
-    val _ = Output.status (Markup.markup Markup.forked "");
+    val task_props =
+      (case worker_task () of
+        NONE => I
+      | SOME task => Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]);
+    val _ = Output.status (Markup.markup (task_props Markup.forked) "");
     val x = e ();  (*sic -- report "joined" only for success*)
-    val _ = Output.status (Markup.markup Markup.joined "");
+    val _ = Output.status (Markup.markup (task_props Markup.joined) "");
   in x end;
 
 
diff -r 2269544b6457 -r 34823a2cba08 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Pure/Concurrent/synchronized.ML	Wed Nov 10 16:05:15 2010 +0100
@@ -13,6 +13,7 @@
   val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
   val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
   val change: 'a var -> ('a -> 'a) -> unit
+  val counter: unit -> unit -> int
 end;
 
 structure Synchronized: SYNCHRONIZED =
@@ -65,4 +66,17 @@
 
 end;
 
+
+(* unique identifiers > 0 *)
+
+fun counter () =
+  let
+    val counter = var "counter" 0;
+    fun next () =
+      change_result counter
+        (fn i =>
+          let val j = i + 1
+          in (j, j) end);
+  in next end;
+
 end;
diff -r 2269544b6457 -r 34823a2cba08 src/Pure/Concurrent/synchronized_sequential.ML
--- a/src/Pure/Concurrent/synchronized_sequential.ML	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Pure/Concurrent/synchronized_sequential.ML	Wed Nov 10 16:05:15 2010 +0100
@@ -24,4 +24,15 @@
 fun change var f = change_result var (fn x => ((), f x));
 
 end;
+
+fun counter () =
+  let
+    val counter = var "counter" 0;
+    fun next () =
+      change_result counter
+        (fn i =>
+          let val j = i + 1
+          in (j, j) end);
+  in next end;
+
 end;
diff -r 2269544b6457 -r 34823a2cba08 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Nov 10 16:05:15 2010 +0100
@@ -38,13 +38,16 @@
 structure Task_Queue: TASK_QUEUE =
 struct
 
+val new_id = Synchronized.counter ();
+
+
 (* tasks *)
 
-abstype task = Task of int option * serial
+abstype task = Task of int option * int
 with
 
 val dummy_task = Task (NONE, ~1);
-fun new_task pri = Task (pri, serial ());
+fun new_task pri = Task (pri, new_id ());
 
 fun pri_of_task (Task (pri, _)) = the_default 0 pri;
 fun str_of_task (Task (_, i)) = string_of_int i;
@@ -61,13 +64,13 @@
 
 abstype group = Group of
  {parent: group option,
-  id: serial,
+  id: int,
   status: exn list Synchronized.var}
 with
 
 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
 
-fun new_group parent = make_group (parent, serial (), Synchronized.var "group" []);
+fun new_group parent = make_group (parent, new_id (), Synchronized.var "group" []);
 
 fun group_id (Group {id, ...}) = id;
 fun eq_group (group1, group2) = group_id group1 = group_id group2;
diff -r 2269544b6457 -r 34823a2cba08 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Pure/General/yxml.scala	Wed Nov 10 16:05:15 2010 +0100
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import scala.collection.mutable.ListBuffer
+import scala.collection.mutable
 
 
 object YXML
@@ -84,8 +84,8 @@
   {
     /* stack operations */
 
-    def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
-    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
+    def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
+    var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
 
     def add(x: XML.Tree)
     {
diff -r 2269544b6457 -r 34823a2cba08 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Pure/Isar/keyword.scala	Wed Nov 10 16:05:15 2010 +0100
@@ -21,6 +21,7 @@
   val THY_DECL = "theory-decl"
   val THY_SCRIPT = "theory-script"
   val THY_GOAL = "theory-goal"
+  val THY_SCHEMATIC_GOAL = "theory-schematic-goal"
   val QED = "qed"
   val QED_BLOCK = "qed-block"
   val QED_GLOBAL = "qed-global"
@@ -41,9 +42,14 @@
   val minor = Set(MINOR)
   val control = Set(CONTROL)
   val diag = Set(DIAG)
-  val heading = Set(THY_HEADING, PRF_HEADING)
+  val theory =
+    Set(THY_BEGIN, THY_SWITCH, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT,
+      THY_GOAL, THY_SCHEMATIC_GOAL)
   val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
+  val proof =
+    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK,
+      PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
   val proof1 =
     Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
diff -r 2269544b6457 -r 34823a2cba08 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 16:05:15 2010 +0100
@@ -33,11 +33,29 @@
   def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
 
   def is_command(name: String): Boolean =
-    keywords.get(name) match {
+    keyword_kind(name) match {
       case Some(kind) => kind != Keyword.MINOR
       case None => false
     }
 
+  def heading_level(name: String): Option[Int] =
+    name match {
+      // FIXME avoid hard-wired info!?
+      case "header" => Some(1)
+      case "chapter" => Some(2)
+      case "section" | "sect" => Some(3)
+      case "subsection" | "subsect" => Some(4)
+      case "subsubsection" | "subsubsect" => Some(5)
+      case _ =>
+        keyword_kind(name) match {
+          case Some(kind) if Keyword.theory(kind) => Some(6)
+          case _ => None
+        }
+    }
+
+  def heading_level(command: Command): Option[Int] =
+    heading_level(command.name)
+
 
   /* tokenize */
 
diff -r 2269544b6457 -r 34823a2cba08 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Nov 10 16:05:15 2010 +0100
@@ -74,10 +74,13 @@
   }
 
 
-  /* unparsed dummy commands */
+  /* dummy commands */
 
-  def unparsed(source: String) =
+  def unparsed(source: String): Command =
     new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
+
+  def span(toks: List[Token]): Command =
+    new Command(Document.NO_ID, toks)
 }
 
 
diff -r 2269544b6457 -r 34823a2cba08 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Nov 10 16:05:15 2010 +0100
@@ -34,16 +34,7 @@
 type exec_id = id;
 
 val no_id = 0;
-
-local
-  val id_count = Synchronized.var "id" 0;
-in
-  fun new_id () =
-    Synchronized.change_result id_count
-      (fn i =>
-        let val i' = i + 1
-        in (i', i') end);
-end;
+val new_id = Synchronized.counter ();
 
 val parse_id = Markup.parse_int;
 val print_id = Markup.print_int;
diff -r 2269544b6457 -r 34823a2cba08 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Nov 10 16:05:15 2010 +0100
@@ -13,6 +13,70 @@
 
 object Thy_Syntax
 {
+  /** nested structure **/
+
+  object Structure
+  {
+    sealed abstract class Entry
+    {
+      def length: Int
+    }
+    case class Block(val name: String, val body: List[Entry]) extends Entry
+    {
+      val length: Int = (0 /: body)(_ + _.length)
+    }
+    case class Atom(val command: Command) extends Entry
+    {
+      def length: Int = command.length
+    }
+
+    def parse_sections(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
+    {
+      /* stack operations */
+
+      def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
+      var stack: List[(Int, String, mutable.ListBuffer[Entry])] = List((0, root_name, buffer()))
+
+      @tailrec def close(level: Int => Boolean)
+      {
+        stack match {
+          case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
+            body2 += Block(name, body.toList)
+            stack = stack.tail
+            close(level)
+          case _ =>
+        }
+      }
+
+      def result(): Entry =
+      {
+        close(_ => true)
+        val (_, name, body) = stack.head
+        Block(name, body.toList)
+      }
+
+      def add(command: Command)
+      {
+        syntax.heading_level(command) match {
+          case Some(i) =>
+            close(_ >= i)
+            stack = (i, command.source, buffer()) :: stack
+          case None =>
+        }
+        stack.head._3 += Atom(command)
+      }
+
+
+      /* result structure */
+
+      val spans = parse_spans(syntax.scan(text))
+      spans.foreach(span => add(Command.span(span)))
+      result()
+    }
+  }
+
+
+
   /** parse spans **/
 
   def parse_spans(toks: List[Token]): List[List[Token]] =
diff -r 2269544b6457 -r 34823a2cba08 src/Tools/jEdit/README_BUILD
--- a/src/Tools/jEdit/README_BUILD	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Tools/jEdit/README_BUILD	Wed Nov 10 16:05:15 2010 +0100
@@ -31,7 +31,7 @@
 * Isabelle/Pure Scala components
   Netbeans Library "Isabelle-Pure" = ~~/lib/classes/Pure.jar
 
-* Scala Compiler 2.8.0.final
+* Scala Compiler 2.8.1.final
   http://www.scala-lang.org
   Netbeans Library "Scala-compiler" = $SCALA_HOME/lib/scala-compiler.jar
 
diff -r 2269544b6457 -r 34823a2cba08 src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Wed Nov 10 16:05:15 2010 +0100
@@ -184,6 +184,8 @@
 line-end.shortcut=END
 line-home.shortcut=HOME
 lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
+mode.isabelle.customSettings=true
+mode.isabelle.folding=sidekick
 mode.isabelle.sidekick.showStatusWindow.label=true
 print.font=IsabelleText
 sidekick-tree.dock-position=right
diff -r 2269544b6457 -r 34823a2cba08 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 09:03:07 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 16:05:15 2010 +0100
@@ -24,8 +24,25 @@
 
 object Isabelle_Sidekick
 {
-  implicit def int_to_pos(offset: Int): Position =
+  def int_to_pos(offset: Int): Position =
     new Position { def getOffset = offset; override def toString = offset.toString }
+
+  class Asset(name: String, start: Int, end: Int) extends IAsset
+  {
+    protected var _name = name
+    protected var _start = int_to_pos(start)
+    protected var _end = int_to_pos(end)
+    override def getIcon: Icon = null
+    override def getShortString: String = _name
+    override def getLongString: String = _name
+    override def getName: String = _name
+    override def setName(name: String) = _name = name
+    override def getStart: Position = _start
+    override def setStart(start: Position) = _start = start
+    override def getEnd: Position = _end
+    override def setEnd(end: Position) = _end = end
+    override def toString = _name
+  }
 }
 
 
@@ -40,14 +57,12 @@
 
   def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
   {
-    import Isabelle_Sidekick.int_to_pos
-
     stopped = false
 
     // FIXME lock buffer (!??)
     val data = new SideKickParsedData(buffer.getName)
     val root = data.root
-    data.getAsset(root).setEnd(buffer.getLength)
+    data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
 
     Swing_Thread.now { Document_Model(buffer) } match {
       case Some(model) =>
@@ -95,32 +110,38 @@
 
 class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
 {
+  import Thy_Syntax.Structure
+
   def parser(data: SideKickParsedData, model: Document_Model)
   {
-    import Isabelle_Sidekick.int_to_pos
+    val syntax = model.session.current_syntax()
 
-    val root = data.root
-    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
-    for {
-      (command, command_start) <- snapshot.node.command_range()
-      if command.is_command && !stopped
-    }
-    {
-      val name = command.name
-      val node =
-        new DefaultMutableTreeNode(new IAsset {
-          override def getIcon: Icon = null
-          override def getShortString: String = name
-          override def getLongString: String = name
-          override def getName: String = name
-          override def setName(name: String) = ()
-          override def setStart(start: Position) = ()
-          override def getStart: Position = command_start
-          override def setEnd(end: Position) = ()
-          override def getEnd: Position = command_start + command.length
-          override def toString = name})
-      root.add(node)
-    }
+    def make_tree(offset: Int, entry: Structure.Entry): List[DefaultMutableTreeNode] =
+      entry match {
+        case Structure.Block(name, body) =>
+          val node =
+            new DefaultMutableTreeNode(
+              new Isabelle_Sidekick.Asset(name, offset, offset + entry.length))
+          (offset /: body)((i, e) =>
+            {
+              make_tree(i, e) foreach (nd => node.add(nd))
+              i + e.length
+            })
+          List(node)
+        case Structure.Atom(command)
+        if command.is_command && syntax.heading_level(command).isEmpty =>
+          val node =
+            new DefaultMutableTreeNode(
+              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
+          List(node)
+        case _ => Nil
+      }
+
+    val buffer = model.buffer
+    val text = Isabelle.buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+    val structure = Structure.parse_sections(syntax, "theory " + model.thy_name, text)
+
+    make_tree(0, structure) foreach (node => data.root.add(node))
   }
 }
 
@@ -129,8 +150,6 @@
 {
   def parser(data: SideKickParsedData, model: Document_Model)
   {
-    import Isabelle_Sidekick.int_to_pos
-
     val root = data.root
     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
@@ -145,18 +164,12 @@
                 case x => x.toString
               }
 
-            new DefaultMutableTreeNode(new IAsset {
-              override def getIcon: Icon = null
-              override def getShortString: String = content
-              override def getLongString: String = info_text
-              override def getName: String = command.toString
-              override def setName(name: String) = ()
-              override def setStart(start: Position) = ()
-              override def getStart: Position = range.start
-              override def setEnd(end: Position) = ()
-              override def getEnd: Position = range.stop
-              override def toString = "\"" + content + "\" " + range.toString
-            })
+            new DefaultMutableTreeNode(
+              new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
+                override def getShortString: String = content
+                override def getLongString: String = info_text
+                override def toString = "\"" + content + "\" " + range.toString
+              })
           })
     }
   }