# HG changeset patch
# User wenzelm
# Date 1313263681 -7200
# Node ID be78e13a80d6182822e96dd8ab14634a9263db26
# Parent  fe55049849373a08e3b2e904980b7dad888c2207# Parent  9e6698b9dcea204a819a5773fd8d7fe915849d71
merged

diff -r fe5504984937 -r be78e13a80d6 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/General/symbol.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -179,7 +179,7 @@
         tab.get(x) match {
           case None => tab += (x -> y)
           case Some(z) =>
-            error("Duplicate mapping of \"" + x + "\" to \"" + y + "\" vs. \"" + z + "\"")
+            error("Duplicate mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z))
         }
       }
       tab
diff -r fe5504984937 -r be78e13a80d6 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/General/yxml.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -50,7 +50,7 @@
   private def err_element() = err("bad element")
   private def err_unbalanced(name: String) =
     if (name == "") err("unbalanced element")
-    else err("unbalanced element \"" + name + "\"")
+    else err("unbalanced element " + quote(name))
 
   private def parse_attrib(source: CharSequence) = {
     val s = source.toString
diff -r fe5504984937 -r be78e13a80d6 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/Isar/isar_syn.ML	Sat Aug 13 21:28:01 2011 +0200
@@ -30,9 +30,10 @@
   Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
     (Thy_Header.args >> (fn (name, imports, uses) =>
       Toplevel.print o
-        Toplevel.init_theory NONE name
-          (fn master =>
-            Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses))));
+        Toplevel.init_theory
+          (fn () =>
+            Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ())
+              name imports (map (apfst Path.explode) uses))));
 
 val _ =
   Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
diff -r fe5504984937 -r be78e13a80d6 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 21:28:01 2011 +0200
@@ -35,7 +35,7 @@
   type isar
   val isar: TextIO.instream -> bool -> isar
   val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
-  val prepare_element: outer_syntax -> (Path.T option -> theory) -> Thy_Syntax.element ->
+  val prepare_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     (Toplevel.transition * Toplevel.transition list) list
   val prepare_command: Position.T -> string -> Toplevel.transition
 end;
@@ -224,7 +224,7 @@
 fun process_file path thy =
   let
     val trs = parse (Path.position path) (File.read path);
-    val init = Toplevel.init_theory NONE "" (K thy) Toplevel.empty;
+    val init = Toplevel.init_theory (K thy) Toplevel.empty;
     val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
   in
     (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
diff -r fe5504984937 -r be78e13a80d6 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/Isar/parse.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -50,7 +50,7 @@
       token(s, pred) ^^ (_.content)
 
     def keyword(name: String): Parser[String] =
-      atom(Token.Kind.KEYWORD.toString + " \"" + name + "\"",
+      atom(Token.Kind.KEYWORD.toString + " " + quote(name),
         tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
 
     def name: Parser[String] = atom("name declaration", _.is_name)
diff -r fe5504984937 -r be78e13a80d6 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/Isar/toplevel.ML	Sat Aug 13 21:28:01 2011 +0200
@@ -34,7 +34,6 @@
   val thread: bool -> (unit -> unit) -> Thread.thread
   type transition
   val empty: transition
-  val init_of: transition -> string option
   val print_of: transition -> bool
   val name_of: transition -> string
   val pos_of: transition -> Position.T
@@ -45,9 +44,9 @@
   val set_print: bool -> transition -> transition
   val print: transition -> transition
   val no_timing: transition -> transition
-  val init_theory: Path.T option -> string -> (Path.T option -> theory) -> transition -> transition
-  val modify_master: Path.T option -> transition -> transition
-  val modify_init: (Path.T option -> theory) -> transition -> transition
+  val init_theory: (unit -> theory) -> transition -> transition
+  val is_init: transition -> bool
+  val modify_init: (unit -> theory) -> transition -> transition
   val exit: transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
@@ -186,8 +185,8 @@
   | _ => raise UNDEF);
 
 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
-  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos)
-  | end_theory pos (State (NONE, NONE)) = error ("Missing theory " ^ Position.str_of pos);
+  | end_theory pos (State (NONE, _)) = error ("Missing theory " ^ Position.str_of pos)
+  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos);
 
 
 (* print state *)
@@ -297,16 +296,16 @@
 (* primitive transitions *)
 
 datatype trans =
-  Init of Path.T option * string * (Path.T option -> theory) | (*master dir, theory name, init*)
+  Init of unit -> theory |               (*init theory*)
   Exit |                                 (*formal exit of theory*)
   Keep of bool -> state -> unit |        (*peek at state*)
   Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
 
 local
 
-fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
+fun apply_tr _ (Init f) (State (NONE, _)) =
       State (SOME (Theory (Context.Theory
-          (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
+          (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
   | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
       exit_transaction state
   | apply_tr int (Keep f) state =
@@ -353,10 +352,6 @@
 
 (* diagnostics *)
 
-fun get_init (Transition {trans = [Init args], ...}) = SOME args
-  | get_init _ = NONE;
-
-val init_of = Option.map #2 o get_init;
 fun print_of (Transition {print, ...}) = print;
 fun name_of (Transition {name, ...}) = name;
 fun pos_of (Transition {pos, ...}) = pos;
@@ -397,17 +392,12 @@
 
 (* basic transitions *)
 
-fun init_theory master name f = add_trans (Init (master, name, f));
+fun init_theory f = add_trans (Init f);
 
-fun modify_master master tr =
-  (case get_init tr of
-    SOME (_, name, f) => init_theory master name f (reset_trans tr)
-  | NONE => tr);
+fun is_init (Transition {trans = [Init _], ...}) = true
+  | is_init _ = false;
 
-fun modify_init f tr =
-  (case get_init tr of
-    SOME (master, name, _) => init_theory master name f (reset_trans tr)
-  | NONE => tr);
+fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr;
 
 val exit = add_trans Exit;
 val keep' = add_trans o Keep;
diff -r fe5504984937 -r be78e13a80d6 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/PIDE/document.ML	Sat Aug 13 21:28:01 2011 +0200
@@ -15,10 +15,11 @@
   val new_id: unit -> id
   val parse_id: string -> id
   val print_id: id -> string
+  type node_header = (string * string list * (string * bool) list) Exn.result
   datatype node_edit =
-    Remove |
+    Clear |
     Edits of (command_id option * command_id option) list |
-    Update_Header of (string * string list * string list) Exn.result
+    Header of node_header
   type edit = string * node_edit
   type state
   val init_state: state
@@ -54,33 +55,46 @@
 
 (** document structure **)
 
+type node_header = (string * string list * (string * bool) list) Exn.result;
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
 abstype node = Node of
-  {last: exec_id, entries: exec_id option Entries.T}  (*command entries with excecutions*)
+ {header: node_header,
+  entries: exec_id option Entries.T,  (*command entries with excecutions*)
+  last: exec_id}  (*last entry with main result*)
 and version = Version of node Graph.T  (*development graph wrt. static imports*)
 with
 
-fun make_node (last, entries) =
-  Node {last = last, entries = entries};
+fun make_node (header, entries, last) =
+  Node {header = header, entries = entries, last = last};
 
-fun get_last (Node {last, ...}) = last;
-fun set_last last (Node {entries, ...}) = make_node (last, entries);
+fun map_node f (Node {header, entries, last}) =
+  make_node (f (header, entries, last));
 
-fun map_entries f (Node {last, entries}) = make_node (last, f entries);
+fun get_header (Node {header, ...}) = header;
+fun set_header header = map_node (fn (_, entries, last) => (header, entries, last));
+
+fun map_entries f (Node {header, entries, last}) = make_node (header, f entries, last);
 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
 
-val empty_node = make_node (no_id, Entries.empty);
-val empty_version = Version Graph.empty;
+fun get_last (Node {last, ...}) = last;
+fun set_last last = map_node (fn (header, entries, _) => (header, entries, last));
+
+val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, no_id);
+val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, no_id));
+
+fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
+fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
+fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f;
 
 
 (* node edits and associated executions *)
 
 datatype node_edit =
-  Remove |
+  Clear |
   Edits of (command_id option * command_id option) list |
-  Update_Header of (string * string list * string list) Exn.result;
+  Header of node_header;
 
 type edit = string * node_edit;
 
@@ -104,21 +118,30 @@
 
 (* version operations *)
 
+val empty_version = Version Graph.empty;
+
 fun nodes_of (Version nodes) = nodes;
+val node_of = get_node o nodes_of;
 val node_names_of = Graph.keys o nodes_of;
 
-fun get_node version name = Graph.get_node (nodes_of version) name
-  handle Graph.UNDEF _ => empty_node;
+fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
 
 fun edit_nodes (name, node_edit) (Version nodes) =
   Version
     (case node_edit of
-      Remove => perhaps (try (Graph.del_node name)) nodes
-    | Edits edits =>
-        nodes
-        |> Graph.default_node (name, empty_node)
-        |> Graph.map_node name (edit_node edits)
-    | Update_Header _ => nodes);  (* FIXME *)
+      Clear => update_node name clear_node nodes
+    | Edits edits => update_node name (edit_node edits) nodes
+    | Header header =>
+        let
+          val node = get_node nodes name;
+          val nodes' = Graph.new_node (name, node) (remove_node name nodes);
+          val parents =
+            (case header of Exn.Res (_, parents, _) => parents | _ => [])
+            |> filter (can (Graph.get_node nodes'));
+          val (header', nodes'') =
+            (header, Graph.add_deps_acyclic (name, parents) nodes')
+              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes');
+        in Graph.map_node name (set_header header') nodes'' end);
 
 fun put_node name node (Version nodes) =
   Version (nodes
@@ -203,8 +226,11 @@
 
 fun get_theory state version_id pos name =
   let
-    val last = get_last (get_node (the_version state version_id) name);
-    val st = #2 (Lazy.force (the_exec state last));
+    val last = get_last (node_of (the_version state version_id) name);
+    val st =
+      (case Lazy.peek (the_exec state last) of
+        SOME result => #2 (Exn.release result)
+      | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos));
   in Toplevel.end_theory pos st end;
 
 
@@ -249,41 +275,38 @@
 
 in
 
-fun run_command node_name raw_tr st =
-  (case
-      (case Toplevel.init_of raw_tr of
-        SOME name =>
-          Exn.capture (fn () =>
-            let val master_dir = Path.dir (Path.explode node_name);  (* FIXME move to Scala side *)
-            in Toplevel.modify_master (SOME master_dir) raw_tr end) ()
-      | NONE => Exn.Res raw_tr) of
-    Exn.Res tr =>
-      let
-        val is_init = is_some (Toplevel.init_of tr);
-        val is_proof = Keyword.is_proof (Toplevel.name_of tr);
-        val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
+fun run_command (node_name, node_header) raw_tr st =
+  let
+    val is_init = Toplevel.is_init raw_tr;
+    val tr =
+      if is_init then
+        raw_tr |> Toplevel.modify_init (fn () =>
+          let
+            (* FIXME get theories from document state *)
+            (* FIXME provide files via Scala layer *)
+            val (name, imports, uses) = Exn.release node_header;
+            val master = Path.dir (Path.explode node_name);
+          in Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses) end)
+      else raw_tr;
 
-        val start = Timing.start ();
-        val (errs, result) =
-          if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
-          else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
-        val _ = timing tr (Timing.result start);
-        val _ = List.app (Toplevel.error_msg tr) errs;
-        val res =
-          (case result of
-            NONE => (Toplevel.status tr Markup.failed; (false, st))
-          | SOME st' =>
-             (Toplevel.status tr Markup.finished;
-              proof_status tr st';
-              if do_print then async_state tr st' else ();
-              (true, st')));
-      in res end
-  | Exn.Exn exn =>
-      if Exn.is_interrupt exn then reraise exn
-      else
-       (Toplevel.error_msg raw_tr (ML_Compiler.exn_message exn);
-        Toplevel.status raw_tr Markup.failed;
-        (false, Toplevel.toplevel)));
+    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
+    val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
+
+    val start = Timing.start ();
+    val (errs, result) =
+      if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
+      else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+    val _ = timing tr (Timing.result start);
+    val _ = List.app (Toplevel.error_msg tr) errs;
+  in
+    (case result of
+      NONE => (Toplevel.status tr Markup.failed; (false, st))
+    | SOME st' =>
+       (Toplevel.status tr Markup.finished;
+        proof_status tr st';
+        if do_print then async_state tr st' else ();
+        (true, st')))
+  end;
 
 end;
 
@@ -301,7 +324,7 @@
     NONE => true
   | SOME exec' => exec' <> exec);
 
-fun new_exec name (id: command_id) (exec_id, updates, state) =
+fun new_exec node_info (id: command_id) (exec_id, updates, state) =
   let
     val exec = the_exec state exec_id;
     val exec_id' = new_id ();
@@ -311,7 +334,7 @@
         let
           val st = #2 (Lazy.force exec);
           val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
-        in run_command name exec_tr st end);
+        in run_command node_info exec_tr st end);
     val state' = define_exec exec_id' exec' state;
   in (exec_id', (id, exec_id') :: updates, state') end;
 
@@ -320,12 +343,15 @@
 fun edit (old_id: version_id) (new_id: version_id) edits state =
   let
     val old_version = the_version state old_id;
-    val _ = Time.now ();  (* FIXME odd workaround *)
+    val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
     val new_version = fold edit_nodes edits old_version;
 
     fun update_node name (rev_updates, version, st) =
-      let val node = get_node version name in
-        (case first_entry NONE (is_changed (get_node old_version name)) node of
+      let
+        val node = node_of version name;
+        val header = get_header node;
+      in
+        (case first_entry NONE (is_changed (node_of old_version name)) node of
           NONE => (rev_updates, version, st)
         | SOME ((prev, id), _) =>
             let
@@ -334,12 +360,12 @@
                   NONE => no_id
                 | SOME prev_id => the_default no_id (the_entry node prev_id));
               val (last, rev_upds, st') =
-                fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
+                fold_entries (SOME id) (new_exec (name, header) o #2 o #1) node (prev_exec, [], st);
               val node' = node |> fold update_entry rev_upds |> set_last last;
             in (rev_upds @ rev_updates, put_node name node' version, st') end)
       end;
 
-    (* FIXME proper node deps *)
+    (* FIXME Graph.schedule *)
     val (rev_updates, new_version', state') =
       fold update_node (node_names_of new_version) ([], new_version, state);
     val state'' = define_version new_id new_version' state';
@@ -360,13 +386,13 @@
       fun force_exec NONE = ()
         | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
 
-      val execution' = (* FIXME proper node deps *)
+      val execution' = (* FIXME Graph.schedule *)
         Future.forks
           {name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true}
           [fn () =>
             node_names_of version |> List.app (fn name =>
               fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
-                  (get_node version name) ())];
+                  (node_of version name) ())];
 
     in (versions, commands, execs, execution') end);
 
diff -r fe5504984937 -r be78e13a80d6 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/PIDE/document.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -36,34 +36,30 @@
   type Edit_Command = Edit[(Option[Command], Option[Command])]
   type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
 
+  type Node_Header = Exn.Result[Thy_Header]
+
   object Node
   {
     sealed abstract class Edit[A]
     {
       def map[B](f: A => B): Edit[B] =
         this match {
-          case Remove() => Remove()
+          case Clear() => Clear()
           case Edits(es) => Edits(es.map(f))
-          case Update_Header(header: Header) => Update_Header(header)
+          case Header(header) => Header(header)
         }
     }
-    case class Remove[A]() extends Edit[A]
+    case class Clear[A]() extends Edit[A]
     case class Edits[A](edits: List[A]) extends Edit[A]
-    case class Update_Header[A](header: Header) extends Edit[A]
+    case class Header[A](header: Node_Header) extends Edit[A]
 
-    sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
-    {
-      def norm_deps(f: (String, Path) => String): Header =
-        copy(thy_header =
-          thy_header match {
-            case Exn.Res(header) =>
-              Exn.capture { header.norm_deps(name => f(master_dir, Path.explode(name))) }
-            case exn => exn
-          })
-    }
-    val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
+    def norm_header[A](f: String => String, header: Node_Header): Header[A] =
+      header match {
+        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f) })
+        case exn => Header[A](exn)
+      }
 
-    val empty: Node = Node(empty_header, Map(), Linear_Set())
+    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set())
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
@@ -80,7 +76,7 @@
   private val block_size = 1024
 
   sealed case class Node(
-    val header: Node.Header,
+    val header: Node_Header,
     val blobs: Map[String, Blob],
     val commands: Linear_Set[Command])
   {
diff -r fe5504984937 -r be78e13a80d6 src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/PIDE/isar_document.ML	Sat Aug 13 21:28:01 2011 +0200
@@ -22,11 +22,12 @@
             let open XML.Decode in
               list (pair string
                 (variant
-                 [fn ([], []) => Document.Remove,
+                 [fn ([], []) => Document.Clear,
                   fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
                   fn ([], a) =>
-                    Document.Update_Header (Exn.Res (triple string (list string) (list string) a)),
-                  fn ([a], []) => Document.Update_Header (Exn.Exn (ERROR a))]))
+                    Document.Header
+                      (Exn.Res (triple string (list string) (list (pair string bool)) a)),
+                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
             end;
 
       val await_cancellation = Document.cancel_execution state;
diff -r fe5504984937 -r be78e13a80d6 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/PIDE/isar_document.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -147,13 +147,11 @@
       def encode: T[List[Document.Edit_Command_ID]] =
         list(pair(string,
           variant(List(
-            { case Document.Node.Remove() => (Nil, Nil) },
+            { case Document.Node.Clear() => (Nil, Nil) },
             { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
-            { case Document.Node.Update_Header(
-                  Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
-                (Nil, triple(string, list(string), list(string))(a, b, c)) },
-            { case Document.Node.Update_Header(
-                  Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
+            { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
+                (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
+            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
       YXML.string_of_body(encode(edits)) }
 
     input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
diff -r fe5504984937 -r be78e13a80d6 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/ROOT.ML	Sat Aug 13 21:28:01 2011 +0200
@@ -243,10 +243,10 @@
 use "Thy/thy_output.ML";
 use "Thy/thy_syntax.ML";
 use "Isar/outer_syntax.ML";
-use "PIDE/document.ML";
 use "Thy/present.ML";
 use "Thy/thy_load.ML";
 use "Thy/thy_info.ML";
+use "PIDE/document.ML";
 use "Thy/rail.ML";
 
 (*theory and proof operations*)
diff -r fe5504984937 -r be78e13a80d6 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/System/isabelle_system.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -47,8 +47,6 @@
     if (_state.isEmpty) {
       import scala.collection.JavaConversions._
 
-      System.err.println("### Isabelle system initialization")
-
       val standard_system = new Standard_System
       val settings =
       {
diff -r fe5504984937 -r be78e13a80d6 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/System/session.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -164,8 +164,10 @@
 
   private case class Start(timeout: Time, args: List[String])
   private case object Interrupt
-  private case class Init_Node(name: String, header: Document.Node.Header, text: String)
-  private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
+  private case class Init_Node(
+    name: String, master_dir: String, header: Document.Node_Header, text: String)
+  private case class Edit_Node(
+    name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
   private case class Change_Node(
     name: String,
     doc_edits: List[Document.Edit_Command],
@@ -180,18 +182,20 @@
 
     /* incoming edits */
 
-    def handle_edits(name: String,
-        header: Document.Node.Header, edits: List[Document.Node.Edit[Text.Edit]])
+    def handle_edits(name: String, master_dir: String,
+        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit]])
     //{{{
     {
       val syntax = current_syntax()
       val previous = global_state().history.tip.version
-      val doc_edits =
-        (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
-          edits.map(edit => (name, edit))
-      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
+
+      val norm_header =
+        Document.Node.norm_header[Text.Edit](
+          name => file_store.append(master_dir, Path.explode(name)), header)
+      val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
+      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
       val change =
-        global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))
+        global_state.change_yield(_.extend_history(previous, text_edits, result.map(_._2)))
 
       result.map {
         case (doc_edits, _) =>
@@ -325,14 +329,14 @@
         case Interrupt if prover.isDefined =>
           prover.get.interrupt
 
-        case Init_Node(name, header, text) if prover.isDefined =>
+        case Init_Node(name, master_dir, header, text) if prover.isDefined =>
           // FIXME compare with existing node
-          handle_edits(name, header,
-            List(Document.Node.Remove(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
+          handle_edits(name, master_dir, header,
+            List(Document.Node.Clear(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
           reply(())
 
-        case Edit_Node(name, header, text_edits) if prover.isDefined =>
-          handle_edits(name, header, List(Document.Node.Edits(text_edits)))
+        case Edit_Node(name, master_dir, header, text_edits) if prover.isDefined =>
+          handle_edits(name, master_dir, header, List(Document.Node.Edits(text_edits)))
           reply(())
 
         case change: Change_Node if prover.isDefined =>
@@ -360,9 +364,9 @@
 
   def interrupt() { session_actor ! Interrupt }
 
-  def init_node(name: String, header: Document.Node.Header, text: String)
-  { session_actor !? Init_Node(name, header, text) }
+  def init_node(name: String, master_dir: String, header: Document.Node_Header, text: String)
+  { session_actor !? Init_Node(name, master_dir, header, text) }
 
-  def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
-  { session_actor !? Edit_Node(name, header, edits) }
+  def edit_node(name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
+  { session_actor !? Edit_Node(name, master_dir, header, edits) }
 }
diff -r fe5504984937 -r be78e13a80d6 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/Thy/thy_header.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -28,10 +28,10 @@
 
   /* theory file name */
 
-  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
+  private val Thy_Name = new Regex("""(.*?)([^/\\:]+)\.thy""")
 
-  def thy_name(s: String): Option[String] =
-    s match { case Thy_Name(name) => Some(name) case _ => None }
+  def thy_name(s: String): Option[(String, String)] =
+    s match { case Thy_Name(prefix, name) => Some((prefix, name)) case _ => None }
 
   def thy_path(name: String): Path = Path.basic(name).ext("thy")
 
@@ -44,7 +44,8 @@
     val theory_name = atom("theory name", _.is_name)
 
     val file =
-      keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name
+      keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
+      file_name ^^ (x => (x, true))
 
     val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }
 
@@ -106,12 +107,13 @@
 }
 
 
-sealed case class Thy_Header(val name: String, val imports: List[String], val uses: List[String])
+sealed case class Thy_Header(
+  val name: String, val imports: List[String], val uses: List[(String, Boolean)])
 {
   def map(f: String => String): Thy_Header =
-    Thy_Header(f(name), imports.map(f), uses.map(f))
+    Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
 
   def norm_deps(f: String => String): Thy_Header =
-    copy(imports = imports.map(name => f(name) + ".thy"), uses = uses.map(f))
+    copy(imports = imports.map(name => f(name)), uses = uses.map(p => (f(p._1), p._2)))
 }
 
diff -r fe5504984937 -r be78e13a80d6 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/Thy/thy_info.ML	Sat Aug 13 21:28:01 2011 +0200
@@ -21,8 +21,7 @@
   val use_thys_wrt: Path.T -> string list -> unit
   val use_thys: string list -> unit
   val use_thy: string -> unit
-  val toplevel_begin_theory: Path.T option -> string ->
-    string list -> (Path.T * bool) list -> theory
+  val toplevel_begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
 end;
@@ -312,9 +311,8 @@
 
 (* toplevel begin theory -- without maintaining database *)
 
-fun toplevel_begin_theory master name imports uses =
+fun toplevel_begin_theory dir name imports uses =
   let
-    val dir = (case master of SOME dir => dir | NONE => Thy_Load.get_master_path ());
     val _ = kill_thy name;
     val _ = use_thys_wrt dir imports;
     val parents = map (get_theory o base_name) imports;
diff -r fe5504984937 -r be78e13a80d6 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/Thy/thy_load.ML	Sat Aug 13 21:28:01 2011 +0200
@@ -167,7 +167,7 @@
     val time = ! Toplevel.timing;
 
     val _ = Present.init_theory name;
-    fun init _ =
+    fun init () =
       begin_theory dir name imports uses parents
       |> Present.begin_theory update_time dir uses;
 
diff -r fe5504984937 -r be78e13a80d6 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -179,8 +179,8 @@
       var nodes = previous.nodes
 
       edits foreach {
-        case (name, Document.Node.Remove()) =>
-          doc_edits += (name -> Document.Node.Remove())
+        case (name, Document.Node.Clear()) =>
+          doc_edits += (name -> Document.Node.Clear())
           nodes -= name
 
         case (name, Document.Node.Edits(text_edits)) =>
@@ -199,15 +199,17 @@
           doc_edits += (name -> Document.Node.Edits(cmd_edits))
           nodes += (name -> node.copy(commands = commands2))
 
-        case (name, Document.Node.Update_Header(header)) =>
+        case (name, Document.Node.Header(header)) =>
           val node = nodes(name)
           val update_header =
-            (node.header.thy_header, header) match {
-              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header))) =>
-                thy_header0 != thy_header
+            (node.header, header) match {
+              case (Exn.Res(thy_header0), Exn.Res(thy_header)) => thy_header0 != thy_header
               case _ => true
             }
-          if (update_header) doc_edits += (name -> Document.Node.Update_Header(header))
+          if (update_header) {
+            doc_edits += (name -> Document.Node.Header(header))
+            nodes += (name -> node.copy(header = header))
+          }
       }
       (doc_edits.toList, Document.Version(Document.new_id(), nodes))
     }
diff -r fe5504984937 -r be78e13a80d6 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -62,9 +62,8 @@
 {
   /* pending text edits */
 
-  def node_header(): Document.Node.Header =
-    Document.Node.Header(master_dir,
-      Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
+  def node_header(): Exn.Result[Thy_Header] =
+    Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
 
   private object pending_edits  // owned by Swing thread
   {
@@ -78,14 +77,14 @@
         case Nil =>
         case edits =>
           pending.clear
-          session.edit_node(node_name, node_header(), edits)
+          session.edit_node(node_name, master_dir, node_header(), edits)
       }
     }
 
     def init()
     {
       flush()
-      session.init_node(node_name, node_header(), Isabelle.buffer_text(buffer))
+      session.init_node(node_name, master_dir, node_header(), Isabelle.buffer_text(buffer))
     }
 
     private val delay_flush =
diff -r fe5504984937 -r be78e13a80d6 src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -165,7 +165,7 @@
 
   val tooltip: Markup_Tree.Select[String] =
   {
-    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
+    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
     case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
       Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
         margin = Isabelle.Int_Property("tooltip-margin"))
diff -r fe5504984937 -r be78e13a80d6 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -167,7 +167,7 @@
               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
+                override def toString = quote(content) + " " + range.toString
               })
           })
     }
diff -r fe5504984937 -r be78e13a80d6 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sat Aug 13 07:56:55 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Aug 13 21:28:01 2011 +0200
@@ -210,8 +210,8 @@
           case None =>
             val (master_dir, path) = buffer_path(buffer)
             Thy_Header.thy_name(path) match {
-              case Some(name) =>
-                Some(Document_Model.init(session, buffer, master_dir, path, name))
+              case Some((prefix, name)) =>
+                Some(Document_Model.init(session, buffer, master_dir, prefix + name, name))
               case None => None
             }
         }
@@ -327,13 +327,17 @@
 
   private val file_store = new Session.File_Store
   {
-    def append(master_dir: String, path: Path): String =
+    def append(master_dir: String, source_path: Path): String =
     {
-      val vfs = VFSManager.getVFSForPath(master_dir)
-      if (vfs.isInstanceOf[FileVFS])
-        MiscUtilities.resolveSymlinks(
-          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
-      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
+      val path = source_path.expand
+      if (path.is_absolute) Isabelle_System.platform_path(path)
+      else {
+        val vfs = VFSManager.getVFSForPath(master_dir)
+        if (vfs.isInstanceOf[FileVFS])
+          MiscUtilities.resolveSymlinks(
+            vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
+        else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
+      }
     }
 
     def require(canonical_name: String)