# HG changeset patch
# User wenzelm
# Date 1373059059 -7200
# Node ID 64206b5b243cb15e70cc6fbbeced62882b58b052
# Parent  48b52b03915076bc7c39dbf7e48d74b955df9f1e# Parent  4b5941730bd8044148afb01a37812dc5adb4214e
merged

diff -r 48b52b039150 -r 64206b5b243c src/Pure/Concurrent/counter.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/counter.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -0,0 +1,28 @@
+(*  Title:      Pure/Concurrent/counter.ML
+    Author:     Makarius
+
+Synchronized counter for unique identifiers > 0.
+
+NB: ML ticks forwards, JVM ticks backwards.
+*)
+
+signature COUNTER =
+sig
+  val make: unit -> unit -> int
+end;
+
+structure Counter: COUNTER =
+struct
+
+fun make () =
+  let
+    val counter = Synchronized.var "counter" (0: int);
+    fun next () =
+      Synchronized.change_result counter
+        (fn i =>
+          let val j = i + (1: int)
+          in (j, j) end);
+  in next end;
+
+end;
+
diff -r 48b52b039150 -r 64206b5b243c src/Pure/Concurrent/counter.scala
--- a/src/Pure/Concurrent/counter.scala	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Concurrent/counter.scala	Fri Jul 05 23:17:39 2013 +0200
@@ -13,7 +13,7 @@
 object Counter
 {
   type ID = Long
-  def apply(): Counter = new Counter
+  def make(): Counter = new Counter
 }
 
 final class Counter private
diff -r 48b52b039150 -r 64206b5b243c src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -26,7 +26,7 @@
 
 (* type request *)
 
-val request_counter = Synchronized.counter ();
+val request_counter = Counter.make ();
 datatype request = Request of int;
 fun new_request () = Request (request_counter ());
 
diff -r 48b52b039150 -r 64206b5b243c src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -13,7 +13,6 @@
   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 =
@@ -66,17 +65,4 @@
 
 end;
 
-
-(* unique identifiers > 0 *)
-
-fun counter () =
-  let
-    val counter = var "counter" (0: int);
-    fun next () =
-      change_result counter
-        (fn i =>
-          let val j = i + (1: int)
-          in (j, j) end);
-  in next end;
-
 end;
diff -r 48b52b039150 -r 64206b5b243c src/Pure/Concurrent/synchronized_sequential.ML
--- a/src/Pure/Concurrent/synchronized_sequential.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Concurrent/synchronized_sequential.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -25,14 +25,4 @@
 
 end;
 
-fun counter () =
-  let
-    val counter = var "counter" (0: int);
-    fun next () =
-      change_result counter
-        (fn i =>
-          let val j = i + (1: int)
-          in (j, j) end);
-  in next end;
-
 end;
diff -r 48b52b039150 -r 64206b5b243c src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -47,7 +47,7 @@
 structure Task_Queue: TASK_QUEUE =
 struct
 
-val new_id = Synchronized.counter ();
+val new_id = Counter.make ();
 
 
 (** nested groups of tasks **)
diff -r 48b52b039150 -r 64206b5b243c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -81,7 +81,7 @@
   val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
   val skip_proof: (int -> int) -> transition -> transition
   val skip_proof_to_theory: (int -> bool) -> transition -> transition
-  val put_id: int -> transition -> transition
+  val exec_id: Document_ID.exec -> transition -> transition
   val unknown_theory: transition -> transition
   val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
@@ -585,8 +585,8 @@
 
 (* runtime position *)
 
-fun put_id id (tr as Transition {pos, ...}) =
-  position (Position.put_id (Markup.print_int id) pos) tr;
+fun exec_id id (tr as Transition {pos, ...}) =
+  position (Position.put_id (Document_ID.print id) pos) tr;
 
 fun setmp_thread_position (Transition {pos, ...}) f x =
   Position.setmp_thread_data pos f x;
diff -r 48b52b039150 -r 64206b5b243c src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -1,45 +1,33 @@
 (*  Title:      Pure/PIDE/command.ML
     Author:     Makarius
 
-Prover command execution.
+Prover command execution: read -- eval -- print.
 *)
 
 signature COMMAND =
 sig
-  type span = Token.T list
-  val range: span -> Position.range
-  val proper_range: span -> Position.range
-  type 'a memo
-  val memo: (unit -> 'a) -> 'a memo
-  val memo_value: 'a -> 'a memo
-  val memo_eval: 'a memo -> 'a
-  val memo_fork: Future.params -> 'a memo -> unit
-  val memo_result: 'a memo -> 'a
-  val memo_stable: 'a memo -> bool
-  val read: span -> Toplevel.transition
-  type eval_state =
-    {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}
-  type eval = eval_state memo
-  val no_eval: eval
-  val eval: span -> Toplevel.transition -> eval_state -> eval_state
+  type eval_process
+  type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
+  val eval_result_state: eval -> Toplevel.state
+  type print_process
+  type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
+  type exec = eval * print list
+  val no_exec: exec
+  val exec_ids: exec -> Document_ID.exec list
+  val read: (unit -> theory) -> Token.T list -> Toplevel.transition
+  val eval: (unit -> theory) -> Token.T list -> eval -> eval
+  val print: string -> eval -> print list
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
-  type print = {name: string, pri: int, exec_id: int, print: unit memo}
-  val print: (unit -> int) -> string -> eval -> print list
   val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
+  val execute: exec -> unit
+  val stable_eval: eval -> bool
+  val stable_print: print -> bool
 end;
 
 structure Command: COMMAND =
 struct
 
-(* source *)
-
-type span = Token.T list;
-
-val range = Token.position_range_of;
-val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
-
-
-(* memo results *)
+(** memo results -- including physical interrupts! **)
 
 datatype 'a expr =
   Expr of unit -> 'a |
@@ -58,7 +46,7 @@
       Synchronized.guarded_access v
         (fn Result res => SOME (res, Result res)
           | Expr e =>
-              let val res = Exn.capture e ();  (*memoing of physical interrupts!*)
+              let val res = Exn.capture e ();  (*sic!*)
               in SOME (res, Result res) end))
   |> Exn.release;
 
@@ -80,14 +68,40 @@
 end;
 
 
+
+(** main phases of execution **)
+
+(* basic type definitions *)
+
+type eval_state =
+  {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
+val init_eval_state =
+  {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
+
+type eval_process = eval_state memo;
+type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
+
+fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
+val eval_result_state = #state o eval_result;
+
+type print_process = unit memo;
+type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
+
+type exec = eval * print list;
+val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
+
+fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
+
+
 (* read *)
 
-fun read span =
+fun read init span =
   let
     val outer_syntax = #2 (Outer_Syntax.get_syntax ());
     val command_reports = Outer_Syntax.command_reports outer_syntax;
 
-    val proper_range = Position.set_range (proper_range span);
+    val proper_range =
+      Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span)));
     val pos =
       (case find_first Token.is_command span of
         SOME tok => Token.position_of tok
@@ -102,8 +116,8 @@
         [tr] =>
           if Keyword.is_control (Toplevel.name_of tr) then
             Toplevel.malformed pos "Illegal control command"
-          else tr
-      | [] => Toplevel.ignored (Position.set_range (range span))
+          else Toplevel.modify_init init tr
+      | [] => Toplevel.ignored (Position.set_range (Token.position_range_of span))
       | _ => Toplevel.malformed proper_range "Exactly one command expected")
       handle ERROR msg => Toplevel.malformed proper_range msg
   end;
@@ -111,14 +125,6 @@
 
 (* eval *)
 
-type eval_state =
-  {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
-val no_eval_state: eval_state =
-  {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
-
-type eval = eval_state memo;
-val no_eval = memo_value no_eval_state;
-
 local
 
 fun run int tr st =
@@ -139,9 +145,7 @@
     SOME prf => Toplevel.status tr (Proof.status_markup prf)
   | NONE => ());
 
-in
-
-fun eval span tr ({malformed, state = st, ...}: eval_state) =
+fun eval_state span tr ({malformed, state = st, ...}: eval_state) =
   if malformed then
     {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
   else
@@ -170,12 +174,24 @@
           in {failed = false, malformed = malformed', command = tr, state = st'} end)
     end;
 
+in
+
+fun eval init span eval0 =
+  let
+    val exec_id = Document_ID.make ();
+    fun process () =
+      let
+        val tr =
+          Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
+            (fn () => read init span |> Toplevel.exec_id exec_id) ();
+      in eval_state span tr (eval_result eval0) end;
+  in {exec_id = exec_id, eval_process = memo process} end;
+
 end;
 
 
 (* print *)
 
-type print = {name: string, pri: int, exec_id: int, print: unit memo};
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
 local
@@ -192,28 +208,28 @@
 
 in
 
-fun print new_id command_name eval =
+fun print command_name eval =
   rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
     (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
       Exn.Res NONE => NONE
     | Exn.Res (SOME print_fn) =>
         let
-          val exec_id = new_id ();
-          fun body () =
+          val exec_id = Document_ID.make ();
+          fun process () =
             let
-              val {failed, command, state = st', ...} = memo_result eval;
-              val tr = Toplevel.put_id exec_id command;
+              val {failed, command, state = st', ...} = eval_result eval;
+              val tr = Toplevel.exec_id exec_id command;
             in if failed then () else print_error tr (fn () => print_fn tr st') () end;
-        in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
+        in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end
     | Exn.Exn exn =>
         let
-          val exec_id = new_id ();
-          fun body () =
+          val exec_id = Document_ID.make ();
+          fun process () =
             let
-              val {command, ...} = memo_result eval;
-              val tr = Toplevel.put_id exec_id command;
+              val {command, ...} = eval_result eval;
+              val tr = Toplevel.exec_id exec_id command;
             in output_error tr exn end;
-        in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
+        in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end));
 
 fun print_function {name, pri} f =
   Synchronized.change print_functions (fn funs =>
@@ -233,5 +249,22 @@
           (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
     in if do_print then Toplevel.print_state false st' else () end));
 
+
+(* overall execution process *)
+
+fun execute (({eval_process, ...}, prints): exec) =
+ (memo_eval eval_process;
+  prints |> List.app (fn {name, pri, print_process, ...} =>
+    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
+
+fun stable_goals exec_id =
+  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
+
+fun stable_eval ({exec_id, eval_process}: eval) =
+  stable_goals exec_id andalso memo_stable eval_process;
+
+fun stable_print ({exec_id, print_process, ...}: print) =
+  stable_goals exec_id andalso memo_stable print_process;
+
 end;
 
diff -r 48b52b039150 -r 64206b5b243c src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Jul 05 23:17:39 2013 +0200
@@ -2,12 +2,11 @@
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
-Prover commands with semantic state.
+Prover commands with accumulated results from execution.
 */
 
 package isabelle
 
-import java.lang.System
 
 import scala.collection.mutable
 import scala.collection.immutable.SortedMap
@@ -75,7 +74,7 @@
     private def add_status(st: Markup): State = copy(status = st :: status)
     private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
 
-    def + (alt_id: Document.ID, message: XML.Elem): State =
+    def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
@@ -84,7 +83,9 @@
                 state.add_status(markup)
                   .add_markup(Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
 
-              case _ => System.err.println("Ignored status message: " + msg); state
+              case _ =>
+                java.lang.System.err.println("Ignored status message: " + msg)
+                state
             })
 
         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
@@ -104,7 +105,7 @@
                 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
                 state.add_markup(info)
               case _ =>
-                // FIXME System.err.println("Ignored report message: " + msg)
+                // FIXME java.lang.System.err.println("Ignored report message: " + msg)
                 state
             })
         case XML.Elem(Markup(name, atts), body) =>
@@ -122,7 +123,9 @@
                 else st0
 
               st1
-            case _ => System.err.println("Ignored message without serial number: " + message); this
+            case _ =>
+              java.lang.System.err.println("Ignored message without serial number: " + message)
+              this
           }
       }
 
@@ -136,7 +139,7 @@
   type Span = List[Token]
 
   def apply(
-    id: Document.Command_ID,
+    id: Document_ID.Command,
     node_name: Document.Node.Name,
     span: Span,
     results: Results = Results.empty,
@@ -160,16 +163,16 @@
     new Command(id, node_name, span1.toList, source, results, markup)
   }
 
-  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
+  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil)
 
-  def unparsed(id: Document.Command_ID, source: String, results: Results, markup: Markup_Tree)
+  def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
       : Command =
     Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
 
   def unparsed(source: String): Command =
-    unparsed(Document.no_id, source, Results.empty, Markup_Tree.empty)
+    unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
 
-  def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command =
+  def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
   {
     val text = XML.content(body)
     val markup = Markup_Tree.from_XML(body)
@@ -200,16 +203,16 @@
 
 
 final class Command private(
-    val id: Document.Command_ID,
+    val id: Document_ID.Command,
     val node_name: Document.Node.Name,
-    val span: Command.Span,
+    val span: List[Token],
     val source: String,
     val init_results: Command.Results,
     val init_markup: Markup_Tree)
 {
   /* classification */
 
-  def is_undefined: Boolean = id == Document.no_id
+  def is_undefined: Boolean = id == Document_ID.none
   val is_unparsed: Boolean = span.exists(_.is_unparsed)
   val is_unfinished: Boolean = span.exists(_.is_unfinished)
 
diff -r 48b52b039150 -r 64206b5b243c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -2,36 +2,28 @@
     Author:     Makarius
 
 Document as collection of named nodes, each consisting of an editable
-list of commands, with asynchronous read/eval/print processes.
+list of commands, associated with asynchronous execution process.
 *)
 
 signature DOCUMENT =
 sig
-  type id = int
-  type version_id = id
-  type command_id = id
-  type exec_id = id
-  val no_id: id
-  val new_id: unit -> id
-  val parse_id: string -> id
-  val print_id: id -> string
   type node_header = string * Thy_Header.header * string list
   datatype node_edit =
     Clear |    (* FIXME unused !? *)
-    Edits of (command_id option * command_id option) list |
+    Edits of (Document_ID.command option * Document_ID.command option) list |
     Deps of node_header |
-    Perspective of command_id list
+    Perspective of Document_ID.command list
   type edit = string * node_edit
   type state
   val init_state: state
-  val define_command: command_id -> string -> string -> state -> state
-  val remove_versions: version_id list -> state -> state
+  val define_command: Document_ID.command -> string -> string -> state -> state
+  val remove_versions: Document_ID.version list -> state -> state
   val discontinue_execution: state -> unit
   val cancel_execution: state -> unit
   val start_execution: state -> unit
   val timing: bool Unsynchronized.ref
-  val update: version_id -> version_id -> edit list -> state ->
-    (command_id * exec_id list) list * state
+  val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
+    (Document_ID.command * Document_ID.exec list) list * state
   val state: unit -> state
   val change_state: (state -> state) -> unit
 end;
@@ -39,49 +31,19 @@
 structure Document: DOCUMENT =
 struct
 
-(* unique identifiers *)
-
-type id = int;
-type version_id = id;
-type command_id = id;
-type exec_id = id;
-
-val no_id = 0;
-val new_id = Synchronized.counter ();
-
-val parse_id = Markup.parse_int;
-val print_id = Markup.print_int;
-
-fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id);
-fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
-
-
-(* command execution *)
-
-type exec = exec_id * (Command.eval * Command.print list);  (*eval/print process*)
-val no_exec: exec = (no_id, (Command.no_eval, []));
-
-fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
-
-fun exec_result ((_, (eval, _)): exec) = Command.memo_result eval;
-
-fun exec_run ((_, (eval, prints)): exec) =
- (Command.memo_eval eval;
-  prints |> List.app (fn {name, pri, print, ...} =>
-    Command.memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
-
-
-
 (** document structure **)
 
+fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
+fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
+
 type node_header = string * Thy_Header.header * string list;
-type perspective = Inttab.set * command_id option;
-structure Entries = Linear_Set(type key = command_id val ord = int_ord);
+type perspective = Inttab.set * Document_ID.command option;
+structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
 
 abstype node = Node of
  {header: node_header,  (*master directory, theory header, errors*)
   perspective: perspective,  (*visible commands, last visible command*)
-  entries: exec option Entries.T * bool,  (*command entries with excecutions, stable*)
+  entries: Command.exec option Entries.T * bool,  (*command entries with excecutions, stable*)
   result: Command.eval option}  (*result of last execution*)
 and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
 with
@@ -146,6 +108,11 @@
 fun set_result result =
   map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
 
+fun finished_theory node =
+  (case Exn.capture (Command.eval_result_state o the) (get_result node) of
+    Exn.Res st => can (Toplevel.end_theory Position.none) st
+  | _ => false);
+
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
 fun default_node name = String_Graph.default_node (name, empty_node);
@@ -156,9 +123,9 @@
 
 datatype node_edit =
   Clear |
-  Edits of (command_id option * command_id option) list |
+  Edits of (Document_ID.command option * Document_ID.command option) list |
   Deps of node_header |
-  Perspective of command_id list;
+  Perspective of Document_ID.command list;
 
 type edit = string * node_edit;
 
@@ -174,8 +141,8 @@
     NONE => err_undef "command entry" id
   | SOME (exec, _) => exec);
 
-fun the_default_entry node (SOME id) = (id, the_default no_exec (the_entry node id))
-  | the_default_entry _ NONE = (no_id, no_exec);
+fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id))
+  | the_default_entry _ NONE = (Document_ID.none, Command.no_exec);
 
 fun update_entry id exec =
   map_entries (Entries.update (id, exec));
@@ -234,10 +201,20 @@
 
 (** main state -- document structure and execution process **)
 
+type execution =
+ {version_id: Document_ID.version,
+  group: Future.group,
+  running: bool Unsynchronized.ref};
+
+val no_execution =
+ {version_id = Document_ID.none,
+  group = Future.new_group NONE,
+  running = Unsynchronized.ref false};
+
 abstype state = State of
- {versions: version Inttab.table,  (*version_id -> document content*)
-  commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> named span*)
-  execution: version_id * Future.group * bool Unsynchronized.ref}  (*current execution process*)
+ {versions: version Inttab.table,  (*version id -> document content*)
+  commands: (string * Token.T list lazy) Inttab.table,  (*command id -> named span*)
+  execution: execution}  (*current execution process*)
 with
 
 fun make_state (versions, commands, execution) =
@@ -247,98 +224,85 @@
   make_state (f (versions, commands, execution));
 
 val init_state =
-  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty,
-    (no_id, Future.new_group NONE, Unsynchronized.ref false));
+  make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution);
 
 fun execution_of (State {execution, ...}) = execution;
 
 
 (* document versions *)
 
-fun define_version (id: version_id) version =
+fun define_version version_id version =
   map_state (fn (versions, commands, _) =>
     let
-      val versions' = Inttab.update_new (id, version) versions
+      val versions' = Inttab.update_new (version_id, version) versions
         handle Inttab.DUP dup => err_dup "document version" dup;
-      val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
+      val execution' =
+       {version_id = version_id,
+        group = Future.new_group NONE,
+        running = Unsynchronized.ref true};
     in (versions', commands, execution') end);
 
-fun the_version (State {versions, ...}) (id: version_id) =
-  (case Inttab.lookup versions id of
-    NONE => err_undef "document version" id
+fun the_version (State {versions, ...}) version_id =
+  (case Inttab.lookup versions version_id of
+    NONE => err_undef "document version" version_id
   | SOME version => version);
 
-fun delete_version (id: version_id) versions = Inttab.delete id versions
-  handle Inttab.UNDEF _ => err_undef "document version" id;
+fun delete_version version_id versions =
+  Inttab.delete version_id versions
+    handle Inttab.UNDEF _ => err_undef "document version" version_id;
 
 
 (* commands *)
 
-fun define_command (id: command_id) name text =
+fun define_command command_id name text =
   map_state (fn (versions, commands, execution) =>
     let
-      val id_string = print_id id;
-      val span = Lazy.lazy (fn () =>
-        Position.setmp_thread_data (Position.id_only id_string)
-          (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
-            ());
+      val id = Document_ID.print command_id;
+      val span =
+        Lazy.lazy (fn () =>
+          Position.setmp_thread_data (Position.id_only id)
+            (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
       val _ =
-        Position.setmp_thread_data (Position.id_only id_string)
+        Position.setmp_thread_data (Position.id_only id)
           (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
       val commands' =
-        Inttab.update_new (id, (name, span)) commands
+        Inttab.update_new (command_id, (name, span)) commands
           handle Inttab.DUP dup => err_dup "command" dup;
     in (versions, commands', execution) end);
 
-fun the_command (State {commands, ...}) (id: command_id) =
-  (case Inttab.lookup commands id of
-    NONE => err_undef "command" id
+fun the_command (State {commands, ...}) command_id =
+  (case Inttab.lookup commands command_id of
+    NONE => err_undef "command" command_id
   | SOME command => command);
 
 end;
 
-fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
+fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
   let
-    val _ = member (op =) ids (#1 execution) andalso
-      error ("Attempt to remove execution version " ^ print_id (#1 execution));
+    val _ =
+      member (op =) version_ids (#version_id execution) andalso
+        error ("Attempt to remove execution version " ^ Document_ID.print (#version_id execution));
 
-    val versions' = fold delete_version ids versions;
+    val versions' = fold delete_version version_ids versions;
     val commands' =
       (versions', Inttab.empty) |->
         Inttab.fold (fn (_, version) => nodes_of version |>
           String_Graph.fold (fn (_, (node, _)) => node |>
-            iterate_entries (fn ((_, id), _) =>
-              SOME o Inttab.insert (K true) (id, the_command state id))));
+            iterate_entries (fn ((_, command_id), _) =>
+              SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
   in (versions', commands', execution) end);
 
 
-(* consolidated states *)
-
-fun stable_goals exec_id =
-  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
-
-fun stable_eval ((exec_id, (eval, _)): exec) =
-  stable_goals exec_id andalso Command.memo_stable eval;
-
-fun stable_print ({exec_id, print, ...}: Command.print) =
-  stable_goals exec_id andalso Command.memo_stable print;
-
-fun finished_theory node =
-  (case Exn.capture (Command.memo_result o the) (get_result node) of
-    Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
-  | _ => false);
-
-
 
 (** document execution **)
 
-val discontinue_execution = execution_of #> (fn (_, _, running) => running := false);
-val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group);
-val terminate_execution = execution_of #> (fn (_, group, _) => Future.terminate group);
+val discontinue_execution = execution_of #> (fn {running, ...} => running := false);
+val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
+val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group);
 
 fun start_execution state =
   let
-    val (version_id, group, running) = execution_of state;
+    val {version_id, group, running} = execution_of state;
     val _ =
       (singleton o Future.forks)
         {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
@@ -355,7 +319,7 @@
                   (fn () =>
                     iterate_entries (fn (_, opt_exec) => fn () =>
                       (case opt_exec of
-                        SOME exec => if ! running then SOME (exec_run exec) else NONE
+                        SOME exec => if ! running then SOME (Command.execute exec) else NONE
                       | NONE => NONE)) node ()))));
   in () end;
 
@@ -396,10 +360,9 @@
           SOME thy => thy
         | NONE =>
             Toplevel.end_theory (Position.file_only import)
-              (#state
-                (Command.memo_result
-                  (the_default Command.no_eval
-                    (get_result (snd (the (AList.lookup (op =) deps import)))))))));
+              (case get_result (snd (the (AList.lookup (op =) deps import))) of
+                NONE => Toplevel.toplevel
+              | SOME eval => Command.eval_result_state eval)));
     val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
   in Thy_Load.begin_theory master_dir header parents end;
 
@@ -424,10 +387,11 @@
           val same' =
             (case opt_exec of
               NONE => false
-            | SOME (exec_id, exec) =>
+            | SOME (eval, _) =>
                 (case lookup_entry node0 id of
                   NONE => false
-                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_eval (exec_id, exec)));
+                | SOME (eval0, _) =>
+                    #exec_id eval = #exec_id eval0 andalso Command.stable_eval eval));
         in SOME (same', (prev, flags')) end
       else NONE;
     val (same, (common, flags)) =
@@ -439,56 +403,42 @@
     else (common, flags)
   end;
 
+fun illegal_init _ = error "Illegal theory header after end of theory";
+
 fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
   if not proper_init andalso is_none init then NONE
   else
     let
+      val (_, (eval, _)) = command_exec;
       val (command_name, span) = the_command state command_id' ||> Lazy.force;
-
-      fun illegal_init _ = error "Illegal theory header after end of theory";
-      val (modify_init, init') =
-        if Keyword.is_theory_begin command_name then
-          (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
-        else (I, init);
-
-      val exec_id' = new_id ();
-      val eval' =
-        Command.memo (fn () =>
-          let
-            val eval_state = exec_result (snd command_exec);
-            val tr =
-              Position.setmp_thread_data (Position.id_only (print_id exec_id'))
-                (fn () =>
-                  Command.read span
-                  |> modify_init
-                  |> Toplevel.put_id exec_id') ();
-          in Command.eval span tr eval_state end);
-      val prints' = if command_visible then Command.print new_id command_name eval' else [];
-      val command_exec' = (command_id', (exec_id', (eval', prints')));
+      val init' = if Keyword.is_theory_begin command_name then NONE else init;
+      val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
+      val prints' = if command_visible then Command.print command_name eval' else [];
+      val command_exec' = (command_id', (eval', prints'));
     in SOME (command_exec' :: execs, command_exec', init') end;
 
 fun update_prints state node command_id =
   (case the_entry node command_id of
-    SOME (exec_id, (eval, prints)) =>
+    SOME (eval, prints) =>
       let
         val (command_name, _) = the_command state command_id;
-        val new_prints = Command.print new_id command_name eval;
+        val new_prints = Command.print command_name eval;
         val prints' =
           new_prints |> map (fn new_print =>
             (case find_first (fn {name, ...} => name = #name new_print) prints of
-              SOME print => if stable_print print then print else new_print
+              SOME print => if Command.stable_print print then print else new_print
             | NONE => new_print));
       in
         if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
-        else SOME (command_id, (exec_id, (eval, prints')))
+        else SOME (command_id, (eval, prints'))
       end
   | NONE => NONE);
 
 in
 
-fun update (old_id: version_id) (new_id: version_id) edits state =
+fun update old_version_id new_version_id edits state =
   let
-    val old_version = the_version state old_id;
+    val old_version = the_version state old_version_id;
     val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
 
     val nodes = nodes_of new_version;
@@ -526,7 +476,7 @@
                       else last_common state last_visible node0 node;
                     val common_command_exec = the_default_entry node common;
 
-                    val (new_execs, (command_id', (_, (eval', _))), _) =
+                    val (new_execs, (command_id', (eval', _)), _) =
                       ([], common_command_exec, if initial then SOME init else NONE) |>
                       (still_visible orelse node_required) ?
                         iterate_entries_after common
@@ -536,18 +486,19 @@
 
                     val updated_execs =
                       (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
-                        if exists (fn (_, (id', _)) => id = id') new_execs then I
+                        if exists (fn (_, ({exec_id = id', ...}, _)) => id = id') new_execs then I
                         else append (the_list (update_prints state node id)));
 
                     val no_execs =
                       iterate_entries_after common
                         (fn ((_, id0), exec0) => fn res =>
                           if is_none exec0 then NONE
-                          else if exists (fn (_, (id, _)) => id0 = id) updated_execs
+                          else if exists (fn (_, ({exec_id = id, ...}, _)) => id0 = id) updated_execs
                           then SOME res
                           else SOME (id0 :: res)) node0 [];
 
-                    val last_exec = if command_id' = no_id then NONE else SOME command_id';
+                    val last_exec =
+                      if command_id' = Document_ID.none then NONE else SOME command_id';
                     val result =
                       if is_some (after_entry node last_exec) then NONE
                       else SOME eval';
@@ -568,11 +519,11 @@
 
     val command_execs =
       map (rpair []) (maps #1 updated) @
-      map (fn (command_id, exec) => (command_id, exec_ids_of exec)) (maps #2 updated);
+      map (fn (command_id, exec) => (command_id, Command.exec_ids exec)) (maps #2 updated);
     val updated_nodes = map_filter #3 updated;
 
     val state' = state
-      |> define_version new_id (fold put_node updated_nodes new_version);
+      |> define_version new_version_id (fold put_node updated_nodes new_version);
   in (command_execs, state') end;
 
 end;
diff -r 48b52b039150 -r 64206b5b243c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Jul 05 23:17:39 2013 +0200
@@ -13,20 +13,6 @@
 
 object Document
 {
-  /* formal identifiers */
-
-  type ID = Long
-  val ID = Properties.Value.Long
-
-  type Version_ID = ID
-  type Command_ID = ID
-  type Exec_ID = ID
-
-  val no_id: ID = 0
-  val new_id = Counter()
-
-
-
   /** document structure **/
 
   /* individual nodes */
@@ -202,15 +188,15 @@
     val init: Version = new Version()
 
     def make(syntax: Outer_Syntax, nodes: Nodes): Version =
-      new Version(new_id(), syntax, nodes)
+      new Version(Document_ID.make(), syntax, nodes)
   }
 
   final class Version private(
-    val id: Version_ID = no_id,
+    val id: Document_ID.Version = Document_ID.none,
     val syntax: Outer_Syntax = Outer_Syntax.empty,
     val nodes: Nodes = Nodes.empty)
   {
-    def is_init: Boolean = id == no_id
+    def is_init: Boolean = id == Document_ID.none
   }
 
 
@@ -289,7 +275,7 @@
       result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
   }
 
-  type Assign = List[(Document.Command_ID, List[Document.Exec_ID])]  // exec state assignment
+  type Assign = List[(Document_ID.Command, List[Document_ID.Exec])]  // exec state assignment
 
   object State
   {
@@ -301,13 +287,14 @@
     }
 
     final class Assignment private(
-      val command_execs: Map[Command_ID, List[Exec_ID]] = Map.empty,
+      val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty,
       val is_finished: Boolean = false)
     {
       def check_finished: Assignment = { require(is_finished); this }
       def unfinished: Assignment = new Assignment(command_execs, false)
 
-      def assign(add_command_execs: List[(Command_ID, List[Exec_ID])]): Assignment =
+      def assign(
+        add_command_execs: List[(Document_ID.Command, List[Document_ID.Exec])]): Assignment =
       {
         require(!is_finished)
         val command_execs1 =
@@ -324,10 +311,10 @@
   }
 
   final case class State private(
-    val versions: Map[Version_ID, Version] = Map.empty,
-    val commands: Map[Command_ID, Command.State] = Map.empty,  // static markup from define_command
-    val execs: Map[Exec_ID, Command.State] = Map.empty,  // dynamic markup from execution
-    val assignments: Map[Version_ID, State.Assignment] = Map.empty,
+    val versions: Map[Document_ID.Version, Version] = Map.empty,
+    val commands: Map[Document_ID.Command, Command.State] = Map.empty,  // static markup from define_command
+    val execs: Map[Document_ID.Exec, Command.State] = Map.empty,  // dynamic markup from execution
+    val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
     val history: History = History.init)
   {
     private def fail[A]: A = throw new State.Fail(this)
@@ -345,9 +332,9 @@
       copy(commands = commands + (id -> command.init_state))
     }
 
-    def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
+    def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
 
-    def find_command(version: Version, id: ID): Option[(Node, Command)] =
+    def find_command(version: Version, id: Document_ID.Generic): Option[(Node, Command)] =
       commands.get(id) orElse execs.get(id) match {
         case None => None
         case Some(st) =>
@@ -356,13 +343,13 @@
           Some((node, command))
       }
 
-    def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
-    def the_read_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
-    def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
+    def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
+    def the_read_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
+    def the_exec_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
     def the_assignment(version: Version): State.Assignment =
       assignments.getOrElse(version.id, fail)
 
-    def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
+    def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
       execs.get(id) match {
         case Some(st) =>
           val new_st = st + (id, message)
@@ -376,7 +363,7 @@
           }
       }
 
-    def assign(id: Version_ID, command_execs: Assign = Nil): (List[Command], State) =
+    def assign(id: Document_ID.Version, command_execs: Assign = Nil): (List[Command], State) =
     {
       val version = the_version(id)
 
@@ -437,12 +424,12 @@
       }
     }
 
-    def removed_versions(removed: List[Version_ID]): State =
+    def removed_versions(removed: List[Document_ID.Version]): State =
     {
       val versions1 = versions -- removed
       val assignments1 = assignments -- removed
-      var commands1 = Map.empty[Command_ID, Command.State]
-      var execs1 = Map.empty[Exec_ID, Command.State]
+      var commands1 = Map.empty[Document_ID.Command, Command.State]
+      var execs1 = Map.empty[Document_ID.Exec, Command.State]
       for {
         (version_id, version) <- versions1.iterator
         command_execs = assignments1(version_id).command_execs
diff -r 48b52b039150 -r 64206b5b243c src/Pure/PIDE/document_id.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/document_id.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -0,0 +1,36 @@
+(*  Title:      Pure/PIDE/document_id.ML
+    Author:     Makarius
+
+Unique identifiers for document structure.
+
+NB: ML ticks forwards > 0, JVM ticks backwards < 0.
+*)
+
+signature DOCUMENT_ID =
+sig
+  type generic = int
+  type version = generic
+  type command = generic
+  type exec = generic
+  val none: generic
+  val make: unit -> generic
+  val parse: string -> generic
+  val print: generic -> string
+end;
+
+structure Document_ID: DOCUMENT_ID =
+struct
+
+type generic = int;
+type version = generic;
+type command = generic;
+type exec = generic;
+
+val none = 0;
+val make = Counter.make ();
+
+val parse = Markup.parse_int;
+val print = Markup.print_int;
+
+end;
+
diff -r 48b52b039150 -r 64206b5b243c src/Pure/PIDE/document_id.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/document_id.scala	Fri Jul 05 23:17:39 2013 +0200
@@ -0,0 +1,25 @@
+/*  Title:      Pure/PIDE/document_id.scala
+    Author:     Makarius
+
+Unique identifiers for document structure.
+
+NB: ML ticks forwards > 0, JVM ticks backwards < 0.
+*/
+
+package isabelle
+
+
+object Document_ID
+{
+  type Generic = Long
+  type Version = Generic
+  type Command = Generic
+  type Exec = Generic
+
+  val none: Generic = 0
+  val make = Counter.make()
+
+  def apply(id: Generic): String = Properties.Value.Long.apply(id)
+  def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
+}
+
diff -r 48b52b039150 -r 64206b5b243c src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -10,7 +10,7 @@
 val _ =
   Isabelle_Process.protocol_command "Document.define_command"
     (fn [id, name, text] =>
-      Document.change_state (Document.define_command (Document.parse_id id) name text));
+      Document.change_state (Document.define_command (Document_ID.parse id) name text));
 
 val _ =
   Isabelle_Process.protocol_command "Document.discontinue_execution"
@@ -26,8 +26,8 @@
       let
         val _ = Document.cancel_execution state;
 
-        val old_id = Document.parse_id old_id_string;
-        val new_id = Document.parse_id new_id_string;
+        val old_id = Document_ID.parse old_id_string;
+        val new_id = Document_ID.parse new_id_string;
         val edits =
           YXML.parse_body edits_yxml |>
             let open XML.Decode in
diff -r 48b52b039150 -r 64206b5b243c src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Jul 05 23:17:39 2013 +0200
@@ -13,7 +13,7 @@
 
   object Assign
   {
-    def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
+    def unapply(text: String): Option[(Document_ID.Version, Document.Assign)] =
       try {
         import XML.Decode._
         val body = YXML.parse_body(text)
@@ -27,7 +27,7 @@
 
   object Removed
   {
-    def unapply(text: String): Option[List[Document.Version_ID]] =
+    def unapply(text: String): Option[List[Document_ID.Version]] =
       try {
         import XML.Decode._
         Some(list(long)(YXML.parse_body(text)))
@@ -86,7 +86,7 @@
 
   object Command_Timing
   {
-    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
+    def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
       props match {
         case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
           (args, args) match {
@@ -233,7 +233,7 @@
 
   object Dialog_Args
   {
-    def unapply(props: Properties.T): Option[(Document.ID, Long, String)] =
+    def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] =
       (props, props, props) match {
         case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
           Some((id, serial, result))
@@ -243,7 +243,7 @@
 
   object Dialog
   {
-    def unapply(tree: XML.Tree): Option[(Document.ID, Long, String)] =
+    def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] =
       tree match {
         case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
           Some((id, serial, result))
@@ -253,7 +253,7 @@
 
   object Dialog_Result
   {
-    def apply(id: Document.ID, serial: Long, result: String): XML.Elem =
+    def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem =
     {
       val props = Position.Id(id) ::: Markup.Serial(serial)
       XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
@@ -309,7 +309,7 @@
 
   def define_command(command: Command): Unit =
     input("Document.define_command",
-      Document.ID(command.id), encode(command.name), encode(command.source))
+      Document_ID(command.id), encode(command.name), encode(command.source))
 
 
   /* document versions */
@@ -318,7 +318,7 @@
 
   def cancel_execution() { input("Document.cancel_execution") }
 
-  def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
+  def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
     edits: List[Document.Edit_Command])
   {
     val edits_yxml =
@@ -346,7 +346,7 @@
         pair(string, encode_edit(name))(name.node, edit)
       })
       YXML.string_of_body(encode_edits(edits)) }
-    input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
+    input("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
   }
 
   def remove_versions(versions: List[Document.Version])
diff -r 48b52b039150 -r 64206b5b243c src/Pure/ROOT
--- a/src/Pure/ROOT	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/ROOT	Fri Jul 05 23:17:39 2013 +0200
@@ -152,6 +152,7 @@
     "PIDE/active.ML"
     "PIDE/command.ML"
     "PIDE/document.ML"
+    "PIDE/document_id.ML"
     "PIDE/markup.ML"
     "PIDE/protocol.ML"
     "PIDE/xml.ML"
diff -r 48b52b039150 -r 64206b5b243c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/ROOT.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -22,6 +22,7 @@
 use "Concurrent/synchronized.ML";
 if Multithreading.available then ()
 else use "Concurrent/synchronized_sequential.ML";
+use "Concurrent/counter.ML";
 
 use "General/properties.ML";
 use "General/output.ML";
@@ -256,6 +257,7 @@
 
 (*toplevel transactions*)
 use "Isar/proof_node.ML";
+use "PIDE/document_id.ML";
 use "Isar/toplevel.ML";
 
 (*theory documents*)
diff -r 48b52b039150 -r 64206b5b243c src/Pure/System/invoke_scala.ML
--- a/src/Pure/System/invoke_scala.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/System/invoke_scala.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -19,7 +19,7 @@
 
 (* pending promises *)
 
-val new_id = string_of_int o Synchronized.counter ();
+val new_id = string_of_int o Counter.make ();
 
 val promises =
   Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
diff -r 48b52b039150 -r 64206b5b243c src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/System/session.scala	Fri Jul 05 23:17:39 2013 +0200
@@ -26,7 +26,7 @@
   case class Global_Options(options: Options)
   case object Caret_Focus
   case class Raw_Edits(edits: List[Document.Edit_Text])
-  case class Dialog_Result(id: Document.ID, serial: Long, result: String)
+  case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
@@ -374,7 +374,7 @@
           System.err.println("Ignoring prover output: " + output.message.toString)
       }
 
-      def accumulate(state_id: Document.ID, message: XML.Elem)
+      def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
       {
         try {
           val st = global_state >>> (_.accumulate(state_id, message))
@@ -548,6 +548,6 @@
   def update_options(options: Options)
   { session_actor !? Update_Options(options) }
 
-  def dialog_result(id: Document.ID, serial: Long, result: String)
+  def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
   { session_actor ! Session.Dialog_Result(id, serial, result) }
 }
diff -r 48b52b039150 -r 64206b5b243c src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/System/system_channel.scala	Fri Jul 05 23:17:39 2013 +0200
@@ -31,7 +31,7 @@
 
 private object Fifo_Channel
 {
-  private val next_fifo = Counter()
+  private val next_fifo = Counter.make()
 }
 
 private class Fifo_Channel extends System_Channel
diff -r 48b52b039150 -r 64206b5b243c src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Thy/thy_load.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -217,8 +217,7 @@
   let
     fun prepare_span span =
       Thy_Syntax.span_content span
-      |> Command.read
-      |> Toplevel.modify_init init
+      |> Command.read init
       |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
 
     fun element_result span_elem (st, _) =
diff -r 48b52b039150 -r 64206b5b243c src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Jul 05 23:17:39 2013 +0200
@@ -68,7 +68,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command(Document.no_id, node_name, span)))
+      spans.foreach(span => add(Command(Document_ID.none, node_name, span)))
       result()
     }
   }
@@ -77,9 +77,9 @@
 
   /** parse spans **/
 
-  def parse_spans(toks: List[Token]): List[Command.Span] =
+  def parse_spans(toks: List[Token]): List[List[Token]] =
   {
-    val result = new mutable.ListBuffer[Command.Span]
+    val result = new mutable.ListBuffer[List[Token]]
     val span = new mutable.ListBuffer[Token]
 
     def flush() { if (!span.isEmpty) { result += span.toList; span.clear } }
@@ -198,7 +198,7 @@
   /* reparse range of command spans */
 
   @tailrec private def chop_common(
-      cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
+      cmds: List[Command], spans: List[List[Token]]): (List[Command], List[List[Token]]) =
     (cmds, spans) match {
       case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
       case _ => (cmds, spans)
@@ -225,7 +225,7 @@
         commands
       case cmd :: _ =>
         val hook = commands.prev(cmd)
-        val inserted = spans2.map(span => Command(Document.new_id(), name, span))
+        val inserted = spans2.map(span => Command(Document_ID.make(), name, span))
         (commands /: cmds2)(_ - _).append_after(hook, inserted)
     }
   }
diff -r 48b52b039150 -r 64206b5b243c src/Pure/Tools/proof_general.ML
--- a/src/Pure/Tools/proof_general.ML	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML	Fri Jul 05 23:17:39 2013 +0200
@@ -152,7 +152,7 @@
   | opt_attr name (SOME value) = attr name value;
 
 val pgip_id = "dummy";
-val pgip_serial = Synchronized.counter ();
+val pgip_serial = Counter.make ();
 
 fun output_pgip refid refseq content =
   XML.Elem (("pgip",
diff -r 48b52b039150 -r 64206b5b243c src/Pure/build-jars
--- a/src/Pure/build-jars	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/build-jars	Fri Jul 05 23:17:39 2013 +0200
@@ -33,6 +33,7 @@
   Isar/token.scala
   PIDE/command.scala
   PIDE/document.scala
+  PIDE/document_id.scala
   PIDE/markup.scala
   PIDE/markup_tree.scala
   PIDE/protocol.scala
diff -r 48b52b039150 -r 64206b5b243c src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Tools/jEdit/src/active.scala	Fri Jul 05 23:17:39 2013 +0200
@@ -26,7 +26,7 @@
           val buffer = model.buffer
           val snapshot = model.snapshot()
 
-          def try_replace_command(exec_id: Document.ID, s: String)
+          def try_replace_command(exec_id: Document_ID.Exec, s: String)
           {
             snapshot.state.execs.get(exec_id).map(_.command) match {
               case Some(command) =>
diff -r 48b52b039150 -r 64206b5b243c src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jul 05 23:17:39 2013 +0200
@@ -24,7 +24,7 @@
   private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
     formatted_body: XML.Body): (String, Document.State) =
   {
-    val command = Command.rich_text(Document.new_id(), base_results, formatted_body)
+    val command = Command.rich_text(Document_ID.make(), base_results, formatted_body)
     val node_name = command.node_name
     val edits: List[Document.Edit_Text] =
       List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
@@ -38,7 +38,7 @@
     val state1 =
       state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
         .define_version(version1, state0.the_assignment(version0))
-        .assign(version1.id, List(command.id -> List(Document.new_id())))._2
+        .assign(version1.id, List(command.id -> List(Document_ID.make())))._2
 
     (command.source, state1)
   }
diff -r 48b52b039150 -r 64206b5b243c src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Jul 05 23:17:39 2013 +0200
@@ -290,7 +290,7 @@
 
           case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
           if !body.isEmpty =>
-            val entry: Command.Results.Entry = (Document.new_id(), msg)
+            val entry: Command.Results.Entry = (Document_ID.make(), msg)
             Text.Info(snapshot.convert(info_range), entry) :: msgs
         }).toList.flatMap(_.info)
     if (results.isEmpty) None