--- 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;
--- 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;
--- 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;
--- 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;
--- 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)
{
--- 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)
--- 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 */
--- 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)
}
--- 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;
--- 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]] =
--- 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
--- 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
--- 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
+ })
})
}
}