merged
authorwenzelm
Sat Aug 13 21:28:01 2011 +0200 (2011-08-13)
changeset 44191be78e13a80d6
parent 44190 fe5504984937
parent 44188 9e6698b9dcea
child 44192 a32ca9165928
merged
     1.1 --- a/src/Pure/General/symbol.scala	Sat Aug 13 07:56:55 2011 -0700
     1.2 +++ b/src/Pure/General/symbol.scala	Sat Aug 13 21:28:01 2011 +0200
     1.3 @@ -179,7 +179,7 @@
     1.4          tab.get(x) match {
     1.5            case None => tab += (x -> y)
     1.6            case Some(z) =>
     1.7 -            error("Duplicate mapping of \"" + x + "\" to \"" + y + "\" vs. \"" + z + "\"")
     1.8 +            error("Duplicate mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z))
     1.9          }
    1.10        }
    1.11        tab
     2.1 --- a/src/Pure/General/yxml.scala	Sat Aug 13 07:56:55 2011 -0700
     2.2 +++ b/src/Pure/General/yxml.scala	Sat Aug 13 21:28:01 2011 +0200
     2.3 @@ -50,7 +50,7 @@
     2.4    private def err_element() = err("bad element")
     2.5    private def err_unbalanced(name: String) =
     2.6      if (name == "") err("unbalanced element")
     2.7 -    else err("unbalanced element \"" + name + "\"")
     2.8 +    else err("unbalanced element " + quote(name))
     2.9  
    2.10    private def parse_attrib(source: CharSequence) = {
    2.11      val s = source.toString
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Aug 13 07:56:55 2011 -0700
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Aug 13 21:28:01 2011 +0200
     3.3 @@ -30,9 +30,10 @@
     3.4    Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
     3.5      (Thy_Header.args >> (fn (name, imports, uses) =>
     3.6        Toplevel.print o
     3.7 -        Toplevel.init_theory NONE name
     3.8 -          (fn master =>
     3.9 -            Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses))));
    3.10 +        Toplevel.init_theory
    3.11 +          (fn () =>
    3.12 +            Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ())
    3.13 +              name imports (map (apfst Path.explode) uses))));
    3.14  
    3.15  val _ =
    3.16    Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
     4.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 07:56:55 2011 -0700
     4.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 21:28:01 2011 +0200
     4.3 @@ -35,7 +35,7 @@
     4.4    type isar
     4.5    val isar: TextIO.instream -> bool -> isar
     4.6    val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
     4.7 -  val prepare_element: outer_syntax -> (Path.T option -> theory) -> Thy_Syntax.element ->
     4.8 +  val prepare_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     4.9      (Toplevel.transition * Toplevel.transition list) list
    4.10    val prepare_command: Position.T -> string -> Toplevel.transition
    4.11  end;
    4.12 @@ -224,7 +224,7 @@
    4.13  fun process_file path thy =
    4.14    let
    4.15      val trs = parse (Path.position path) (File.read path);
    4.16 -    val init = Toplevel.init_theory NONE "" (K thy) Toplevel.empty;
    4.17 +    val init = Toplevel.init_theory (K thy) Toplevel.empty;
    4.18      val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
    4.19    in
    4.20      (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
     5.1 --- a/src/Pure/Isar/parse.scala	Sat Aug 13 07:56:55 2011 -0700
     5.2 +++ b/src/Pure/Isar/parse.scala	Sat Aug 13 21:28:01 2011 +0200
     5.3 @@ -50,7 +50,7 @@
     5.4        token(s, pred) ^^ (_.content)
     5.5  
     5.6      def keyword(name: String): Parser[String] =
     5.7 -      atom(Token.Kind.KEYWORD.toString + " \"" + name + "\"",
     5.8 +      atom(Token.Kind.KEYWORD.toString + " " + quote(name),
     5.9          tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
    5.10  
    5.11      def name: Parser[String] = atom("name declaration", _.is_name)
     6.1 --- a/src/Pure/Isar/toplevel.ML	Sat Aug 13 07:56:55 2011 -0700
     6.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Aug 13 21:28:01 2011 +0200
     6.3 @@ -34,7 +34,6 @@
     6.4    val thread: bool -> (unit -> unit) -> Thread.thread
     6.5    type transition
     6.6    val empty: transition
     6.7 -  val init_of: transition -> string option
     6.8    val print_of: transition -> bool
     6.9    val name_of: transition -> string
    6.10    val pos_of: transition -> Position.T
    6.11 @@ -45,9 +44,9 @@
    6.12    val set_print: bool -> transition -> transition
    6.13    val print: transition -> transition
    6.14    val no_timing: transition -> transition
    6.15 -  val init_theory: Path.T option -> string -> (Path.T option -> theory) -> transition -> transition
    6.16 -  val modify_master: Path.T option -> transition -> transition
    6.17 -  val modify_init: (Path.T option -> theory) -> transition -> transition
    6.18 +  val init_theory: (unit -> theory) -> transition -> transition
    6.19 +  val is_init: transition -> bool
    6.20 +  val modify_init: (unit -> theory) -> transition -> transition
    6.21    val exit: transition -> transition
    6.22    val keep: (state -> unit) -> transition -> transition
    6.23    val keep': (bool -> state -> unit) -> transition -> transition
    6.24 @@ -186,8 +185,8 @@
    6.25    | _ => raise UNDEF);
    6.26  
    6.27  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
    6.28 -  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos)
    6.29 -  | end_theory pos (State (NONE, NONE)) = error ("Missing theory " ^ Position.str_of pos);
    6.30 +  | end_theory pos (State (NONE, _)) = error ("Missing theory " ^ Position.str_of pos)
    6.31 +  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos);
    6.32  
    6.33  
    6.34  (* print state *)
    6.35 @@ -297,16 +296,16 @@
    6.36  (* primitive transitions *)
    6.37  
    6.38  datatype trans =
    6.39 -  Init of Path.T option * string * (Path.T option -> theory) | (*master dir, theory name, init*)
    6.40 +  Init of unit -> theory |               (*init theory*)
    6.41    Exit |                                 (*formal exit of theory*)
    6.42    Keep of bool -> state -> unit |        (*peek at state*)
    6.43    Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
    6.44  
    6.45  local
    6.46  
    6.47 -fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
    6.48 +fun apply_tr _ (Init f) (State (NONE, _)) =
    6.49        State (SOME (Theory (Context.Theory
    6.50 -          (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
    6.51 +          (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
    6.52    | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
    6.53        exit_transaction state
    6.54    | apply_tr int (Keep f) state =
    6.55 @@ -353,10 +352,6 @@
    6.56  
    6.57  (* diagnostics *)
    6.58  
    6.59 -fun get_init (Transition {trans = [Init args], ...}) = SOME args
    6.60 -  | get_init _ = NONE;
    6.61 -
    6.62 -val init_of = Option.map #2 o get_init;
    6.63  fun print_of (Transition {print, ...}) = print;
    6.64  fun name_of (Transition {name, ...}) = name;
    6.65  fun pos_of (Transition {pos, ...}) = pos;
    6.66 @@ -397,17 +392,12 @@
    6.67  
    6.68  (* basic transitions *)
    6.69  
    6.70 -fun init_theory master name f = add_trans (Init (master, name, f));
    6.71 +fun init_theory f = add_trans (Init f);
    6.72  
    6.73 -fun modify_master master tr =
    6.74 -  (case get_init tr of
    6.75 -    SOME (_, name, f) => init_theory master name f (reset_trans tr)
    6.76 -  | NONE => tr);
    6.77 +fun is_init (Transition {trans = [Init _], ...}) = true
    6.78 +  | is_init _ = false;
    6.79  
    6.80 -fun modify_init f tr =
    6.81 -  (case get_init tr of
    6.82 -    SOME (master, name, _) => init_theory master name f (reset_trans tr)
    6.83 -  | NONE => tr);
    6.84 +fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr;
    6.85  
    6.86  val exit = add_trans Exit;
    6.87  val keep' = add_trans o Keep;
     7.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 13 07:56:55 2011 -0700
     7.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 13 21:28:01 2011 +0200
     7.3 @@ -15,10 +15,11 @@
     7.4    val new_id: unit -> id
     7.5    val parse_id: string -> id
     7.6    val print_id: id -> string
     7.7 +  type node_header = (string * string list * (string * bool) list) Exn.result
     7.8    datatype node_edit =
     7.9 -    Remove |
    7.10 +    Clear |
    7.11      Edits of (command_id option * command_id option) list |
    7.12 -    Update_Header of (string * string list * string list) Exn.result
    7.13 +    Header of node_header
    7.14    type edit = string * node_edit
    7.15    type state
    7.16    val init_state: state
    7.17 @@ -54,33 +55,46 @@
    7.18  
    7.19  (** document structure **)
    7.20  
    7.21 +type node_header = (string * string list * (string * bool) list) Exn.result;
    7.22  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    7.23  
    7.24  abstype node = Node of
    7.25 -  {last: exec_id, entries: exec_id option Entries.T}  (*command entries with excecutions*)
    7.26 + {header: node_header,
    7.27 +  entries: exec_id option Entries.T,  (*command entries with excecutions*)
    7.28 +  last: exec_id}  (*last entry with main result*)
    7.29  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    7.30  with
    7.31  
    7.32 -fun make_node (last, entries) =
    7.33 -  Node {last = last, entries = entries};
    7.34 +fun make_node (header, entries, last) =
    7.35 +  Node {header = header, entries = entries, last = last};
    7.36  
    7.37 -fun get_last (Node {last, ...}) = last;
    7.38 -fun set_last last (Node {entries, ...}) = make_node (last, entries);
    7.39 +fun map_node f (Node {header, entries, last}) =
    7.40 +  make_node (f (header, entries, last));
    7.41  
    7.42 -fun map_entries f (Node {last, entries}) = make_node (last, f entries);
    7.43 +fun get_header (Node {header, ...}) = header;
    7.44 +fun set_header header = map_node (fn (_, entries, last) => (header, entries, last));
    7.45 +
    7.46 +fun map_entries f (Node {header, entries, last}) = make_node (header, f entries, last);
    7.47  fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
    7.48  fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
    7.49  
    7.50 -val empty_node = make_node (no_id, Entries.empty);
    7.51 -val empty_version = Version Graph.empty;
    7.52 +fun get_last (Node {last, ...}) = last;
    7.53 +fun set_last last = map_node (fn (header, entries, _) => (header, entries, last));
    7.54 +
    7.55 +val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, no_id);
    7.56 +val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, no_id));
    7.57 +
    7.58 +fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
    7.59 +fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
    7.60 +fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f;
    7.61  
    7.62  
    7.63  (* node edits and associated executions *)
    7.64  
    7.65  datatype node_edit =
    7.66 -  Remove |
    7.67 +  Clear |
    7.68    Edits of (command_id option * command_id option) list |
    7.69 -  Update_Header of (string * string list * string list) Exn.result;
    7.70 +  Header of node_header;
    7.71  
    7.72  type edit = string * node_edit;
    7.73  
    7.74 @@ -104,21 +118,30 @@
    7.75  
    7.76  (* version operations *)
    7.77  
    7.78 +val empty_version = Version Graph.empty;
    7.79 +
    7.80  fun nodes_of (Version nodes) = nodes;
    7.81 +val node_of = get_node o nodes_of;
    7.82  val node_names_of = Graph.keys o nodes_of;
    7.83  
    7.84 -fun get_node version name = Graph.get_node (nodes_of version) name
    7.85 -  handle Graph.UNDEF _ => empty_node;
    7.86 +fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
    7.87  
    7.88  fun edit_nodes (name, node_edit) (Version nodes) =
    7.89    Version
    7.90      (case node_edit of
    7.91 -      Remove => perhaps (try (Graph.del_node name)) nodes
    7.92 -    | Edits edits =>
    7.93 -        nodes
    7.94 -        |> Graph.default_node (name, empty_node)
    7.95 -        |> Graph.map_node name (edit_node edits)
    7.96 -    | Update_Header _ => nodes);  (* FIXME *)
    7.97 +      Clear => update_node name clear_node nodes
    7.98 +    | Edits edits => update_node name (edit_node edits) nodes
    7.99 +    | Header header =>
   7.100 +        let
   7.101 +          val node = get_node nodes name;
   7.102 +          val nodes' = Graph.new_node (name, node) (remove_node name nodes);
   7.103 +          val parents =
   7.104 +            (case header of Exn.Res (_, parents, _) => parents | _ => [])
   7.105 +            |> filter (can (Graph.get_node nodes'));
   7.106 +          val (header', nodes'') =
   7.107 +            (header, Graph.add_deps_acyclic (name, parents) nodes')
   7.108 +              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes');
   7.109 +        in Graph.map_node name (set_header header') nodes'' end);
   7.110  
   7.111  fun put_node name node (Version nodes) =
   7.112    Version (nodes
   7.113 @@ -203,8 +226,11 @@
   7.114  
   7.115  fun get_theory state version_id pos name =
   7.116    let
   7.117 -    val last = get_last (get_node (the_version state version_id) name);
   7.118 -    val st = #2 (Lazy.force (the_exec state last));
   7.119 +    val last = get_last (node_of (the_version state version_id) name);
   7.120 +    val st =
   7.121 +      (case Lazy.peek (the_exec state last) of
   7.122 +        SOME result => #2 (Exn.release result)
   7.123 +      | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos));
   7.124    in Toplevel.end_theory pos st end;
   7.125  
   7.126  
   7.127 @@ -249,41 +275,38 @@
   7.128  
   7.129  in
   7.130  
   7.131 -fun run_command node_name raw_tr st =
   7.132 -  (case
   7.133 -      (case Toplevel.init_of raw_tr of
   7.134 -        SOME name =>
   7.135 -          Exn.capture (fn () =>
   7.136 -            let val master_dir = Path.dir (Path.explode node_name);  (* FIXME move to Scala side *)
   7.137 -            in Toplevel.modify_master (SOME master_dir) raw_tr end) ()
   7.138 -      | NONE => Exn.Res raw_tr) of
   7.139 -    Exn.Res tr =>
   7.140 -      let
   7.141 -        val is_init = is_some (Toplevel.init_of tr);
   7.142 -        val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   7.143 -        val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
   7.144 +fun run_command (node_name, node_header) raw_tr st =
   7.145 +  let
   7.146 +    val is_init = Toplevel.is_init raw_tr;
   7.147 +    val tr =
   7.148 +      if is_init then
   7.149 +        raw_tr |> Toplevel.modify_init (fn () =>
   7.150 +          let
   7.151 +            (* FIXME get theories from document state *)
   7.152 +            (* FIXME provide files via Scala layer *)
   7.153 +            val (name, imports, uses) = Exn.release node_header;
   7.154 +            val master = Path.dir (Path.explode node_name);
   7.155 +          in Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses) end)
   7.156 +      else raw_tr;
   7.157  
   7.158 -        val start = Timing.start ();
   7.159 -        val (errs, result) =
   7.160 -          if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
   7.161 -          else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   7.162 -        val _ = timing tr (Timing.result start);
   7.163 -        val _ = List.app (Toplevel.error_msg tr) errs;
   7.164 -        val res =
   7.165 -          (case result of
   7.166 -            NONE => (Toplevel.status tr Markup.failed; (false, st))
   7.167 -          | SOME st' =>
   7.168 -             (Toplevel.status tr Markup.finished;
   7.169 -              proof_status tr st';
   7.170 -              if do_print then async_state tr st' else ();
   7.171 -              (true, st')));
   7.172 -      in res end
   7.173 -  | Exn.Exn exn =>
   7.174 -      if Exn.is_interrupt exn then reraise exn
   7.175 -      else
   7.176 -       (Toplevel.error_msg raw_tr (ML_Compiler.exn_message exn);
   7.177 -        Toplevel.status raw_tr Markup.failed;
   7.178 -        (false, Toplevel.toplevel)));
   7.179 +    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   7.180 +    val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
   7.181 +
   7.182 +    val start = Timing.start ();
   7.183 +    val (errs, result) =
   7.184 +      if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
   7.185 +      else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   7.186 +    val _ = timing tr (Timing.result start);
   7.187 +    val _ = List.app (Toplevel.error_msg tr) errs;
   7.188 +  in
   7.189 +    (case result of
   7.190 +      NONE => (Toplevel.status tr Markup.failed; (false, st))
   7.191 +    | SOME st' =>
   7.192 +       (Toplevel.status tr Markup.finished;
   7.193 +        proof_status tr st';
   7.194 +        if do_print then async_state tr st' else ();
   7.195 +        (true, st')))
   7.196 +  end;
   7.197  
   7.198  end;
   7.199  
   7.200 @@ -301,7 +324,7 @@
   7.201      NONE => true
   7.202    | SOME exec' => exec' <> exec);
   7.203  
   7.204 -fun new_exec name (id: command_id) (exec_id, updates, state) =
   7.205 +fun new_exec node_info (id: command_id) (exec_id, updates, state) =
   7.206    let
   7.207      val exec = the_exec state exec_id;
   7.208      val exec_id' = new_id ();
   7.209 @@ -311,7 +334,7 @@
   7.210          let
   7.211            val st = #2 (Lazy.force exec);
   7.212            val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
   7.213 -        in run_command name exec_tr st end);
   7.214 +        in run_command node_info exec_tr st end);
   7.215      val state' = define_exec exec_id' exec' state;
   7.216    in (exec_id', (id, exec_id') :: updates, state') end;
   7.217  
   7.218 @@ -320,12 +343,15 @@
   7.219  fun edit (old_id: version_id) (new_id: version_id) edits state =
   7.220    let
   7.221      val old_version = the_version state old_id;
   7.222 -    val _ = Time.now ();  (* FIXME odd workaround *)
   7.223 +    val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
   7.224      val new_version = fold edit_nodes edits old_version;
   7.225  
   7.226      fun update_node name (rev_updates, version, st) =
   7.227 -      let val node = get_node version name in
   7.228 -        (case first_entry NONE (is_changed (get_node old_version name)) node of
   7.229 +      let
   7.230 +        val node = node_of version name;
   7.231 +        val header = get_header node;
   7.232 +      in
   7.233 +        (case first_entry NONE (is_changed (node_of old_version name)) node of
   7.234            NONE => (rev_updates, version, st)
   7.235          | SOME ((prev, id), _) =>
   7.236              let
   7.237 @@ -334,12 +360,12 @@
   7.238                    NONE => no_id
   7.239                  | SOME prev_id => the_default no_id (the_entry node prev_id));
   7.240                val (last, rev_upds, st') =
   7.241 -                fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
   7.242 +                fold_entries (SOME id) (new_exec (name, header) o #2 o #1) node (prev_exec, [], st);
   7.243                val node' = node |> fold update_entry rev_upds |> set_last last;
   7.244              in (rev_upds @ rev_updates, put_node name node' version, st') end)
   7.245        end;
   7.246  
   7.247 -    (* FIXME proper node deps *)
   7.248 +    (* FIXME Graph.schedule *)
   7.249      val (rev_updates, new_version', state') =
   7.250        fold update_node (node_names_of new_version) ([], new_version, state);
   7.251      val state'' = define_version new_id new_version' state';
   7.252 @@ -360,13 +386,13 @@
   7.253        fun force_exec NONE = ()
   7.254          | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
   7.255  
   7.256 -      val execution' = (* FIXME proper node deps *)
   7.257 +      val execution' = (* FIXME Graph.schedule *)
   7.258          Future.forks
   7.259            {name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true}
   7.260            [fn () =>
   7.261              node_names_of version |> List.app (fn name =>
   7.262                fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
   7.263 -                  (get_node version name) ())];
   7.264 +                  (node_of version name) ())];
   7.265  
   7.266      in (versions, commands, execs, execution') end);
   7.267  
     8.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 13 07:56:55 2011 -0700
     8.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 13 21:28:01 2011 +0200
     8.3 @@ -36,34 +36,30 @@
     8.4    type Edit_Command = Edit[(Option[Command], Option[Command])]
     8.5    type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
     8.6  
     8.7 +  type Node_Header = Exn.Result[Thy_Header]
     8.8 +
     8.9    object Node
    8.10    {
    8.11      sealed abstract class Edit[A]
    8.12      {
    8.13        def map[B](f: A => B): Edit[B] =
    8.14          this match {
    8.15 -          case Remove() => Remove()
    8.16 +          case Clear() => Clear()
    8.17            case Edits(es) => Edits(es.map(f))
    8.18 -          case Update_Header(header: Header) => Update_Header(header)
    8.19 +          case Header(header) => Header(header)
    8.20          }
    8.21      }
    8.22 -    case class Remove[A]() extends Edit[A]
    8.23 +    case class Clear[A]() extends Edit[A]
    8.24      case class Edits[A](edits: List[A]) extends Edit[A]
    8.25 -    case class Update_Header[A](header: Header) extends Edit[A]
    8.26 +    case class Header[A](header: Node_Header) extends Edit[A]
    8.27  
    8.28 -    sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
    8.29 -    {
    8.30 -      def norm_deps(f: (String, Path) => String): Header =
    8.31 -        copy(thy_header =
    8.32 -          thy_header match {
    8.33 -            case Exn.Res(header) =>
    8.34 -              Exn.capture { header.norm_deps(name => f(master_dir, Path.explode(name))) }
    8.35 -            case exn => exn
    8.36 -          })
    8.37 -    }
    8.38 -    val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
    8.39 +    def norm_header[A](f: String => String, header: Node_Header): Header[A] =
    8.40 +      header match {
    8.41 +        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f) })
    8.42 +        case exn => Header[A](exn)
    8.43 +      }
    8.44  
    8.45 -    val empty: Node = Node(empty_header, Map(), Linear_Set())
    8.46 +    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set())
    8.47  
    8.48      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
    8.49        : Iterator[(Command, Text.Offset)] =
    8.50 @@ -80,7 +76,7 @@
    8.51    private val block_size = 1024
    8.52  
    8.53    sealed case class Node(
    8.54 -    val header: Node.Header,
    8.55 +    val header: Node_Header,
    8.56      val blobs: Map[String, Blob],
    8.57      val commands: Linear_Set[Command])
    8.58    {
     9.1 --- a/src/Pure/PIDE/isar_document.ML	Sat Aug 13 07:56:55 2011 -0700
     9.2 +++ b/src/Pure/PIDE/isar_document.ML	Sat Aug 13 21:28:01 2011 +0200
     9.3 @@ -22,11 +22,12 @@
     9.4              let open XML.Decode in
     9.5                list (pair string
     9.6                  (variant
     9.7 -                 [fn ([], []) => Document.Remove,
     9.8 +                 [fn ([], []) => Document.Clear,
     9.9                    fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    9.10                    fn ([], a) =>
    9.11 -                    Document.Update_Header (Exn.Res (triple string (list string) (list string) a)),
    9.12 -                  fn ([a], []) => Document.Update_Header (Exn.Exn (ERROR a))]))
    9.13 +                    Document.Header
    9.14 +                      (Exn.Res (triple string (list string) (list (pair string bool)) a)),
    9.15 +                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
    9.16              end;
    9.17  
    9.18        val await_cancellation = Document.cancel_execution state;
    10.1 --- a/src/Pure/PIDE/isar_document.scala	Sat Aug 13 07:56:55 2011 -0700
    10.2 +++ b/src/Pure/PIDE/isar_document.scala	Sat Aug 13 21:28:01 2011 +0200
    10.3 @@ -147,13 +147,11 @@
    10.4        def encode: T[List[Document.Edit_Command_ID]] =
    10.5          list(pair(string,
    10.6            variant(List(
    10.7 -            { case Document.Node.Remove() => (Nil, Nil) },
    10.8 +            { case Document.Node.Clear() => (Nil, Nil) },
    10.9              { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
   10.10 -            { case Document.Node.Update_Header(
   10.11 -                  Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
   10.12 -                (Nil, triple(string, list(string), list(string))(a, b, c)) },
   10.13 -            { case Document.Node.Update_Header(
   10.14 -                  Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
   10.15 +            { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
   10.16 +                (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
   10.17 +            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
   10.18        YXML.string_of_body(encode(edits)) }
   10.19  
   10.20      input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
    11.1 --- a/src/Pure/ROOT.ML	Sat Aug 13 07:56:55 2011 -0700
    11.2 +++ b/src/Pure/ROOT.ML	Sat Aug 13 21:28:01 2011 +0200
    11.3 @@ -243,10 +243,10 @@
    11.4  use "Thy/thy_output.ML";
    11.5  use "Thy/thy_syntax.ML";
    11.6  use "Isar/outer_syntax.ML";
    11.7 -use "PIDE/document.ML";
    11.8  use "Thy/present.ML";
    11.9  use "Thy/thy_load.ML";
   11.10  use "Thy/thy_info.ML";
   11.11 +use "PIDE/document.ML";
   11.12  use "Thy/rail.ML";
   11.13  
   11.14  (*theory and proof operations*)
    12.1 --- a/src/Pure/System/isabelle_system.scala	Sat Aug 13 07:56:55 2011 -0700
    12.2 +++ b/src/Pure/System/isabelle_system.scala	Sat Aug 13 21:28:01 2011 +0200
    12.3 @@ -47,8 +47,6 @@
    12.4      if (_state.isEmpty) {
    12.5        import scala.collection.JavaConversions._
    12.6  
    12.7 -      System.err.println("### Isabelle system initialization")
    12.8 -
    12.9        val standard_system = new Standard_System
   12.10        val settings =
   12.11        {
    13.1 --- a/src/Pure/System/session.scala	Sat Aug 13 07:56:55 2011 -0700
    13.2 +++ b/src/Pure/System/session.scala	Sat Aug 13 21:28:01 2011 +0200
    13.3 @@ -164,8 +164,10 @@
    13.4  
    13.5    private case class Start(timeout: Time, args: List[String])
    13.6    private case object Interrupt
    13.7 -  private case class Init_Node(name: String, header: Document.Node.Header, text: String)
    13.8 -  private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
    13.9 +  private case class Init_Node(
   13.10 +    name: String, master_dir: String, header: Document.Node_Header, text: String)
   13.11 +  private case class Edit_Node(
   13.12 +    name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
   13.13    private case class Change_Node(
   13.14      name: String,
   13.15      doc_edits: List[Document.Edit_Command],
   13.16 @@ -180,18 +182,20 @@
   13.17  
   13.18      /* incoming edits */
   13.19  
   13.20 -    def handle_edits(name: String,
   13.21 -        header: Document.Node.Header, edits: List[Document.Node.Edit[Text.Edit]])
   13.22 +    def handle_edits(name: String, master_dir: String,
   13.23 +        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit]])
   13.24      //{{{
   13.25      {
   13.26        val syntax = current_syntax()
   13.27        val previous = global_state().history.tip.version
   13.28 -      val doc_edits =
   13.29 -        (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
   13.30 -          edits.map(edit => (name, edit))
   13.31 -      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
   13.32 +
   13.33 +      val norm_header =
   13.34 +        Document.Node.norm_header[Text.Edit](
   13.35 +          name => file_store.append(master_dir, Path.explode(name)), header)
   13.36 +      val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
   13.37 +      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
   13.38        val change =
   13.39 -        global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))
   13.40 +        global_state.change_yield(_.extend_history(previous, text_edits, result.map(_._2)))
   13.41  
   13.42        result.map {
   13.43          case (doc_edits, _) =>
   13.44 @@ -325,14 +329,14 @@
   13.45          case Interrupt if prover.isDefined =>
   13.46            prover.get.interrupt
   13.47  
   13.48 -        case Init_Node(name, header, text) if prover.isDefined =>
   13.49 +        case Init_Node(name, master_dir, header, text) if prover.isDefined =>
   13.50            // FIXME compare with existing node
   13.51 -          handle_edits(name, header,
   13.52 -            List(Document.Node.Remove(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
   13.53 +          handle_edits(name, master_dir, header,
   13.54 +            List(Document.Node.Clear(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
   13.55            reply(())
   13.56  
   13.57 -        case Edit_Node(name, header, text_edits) if prover.isDefined =>
   13.58 -          handle_edits(name, header, List(Document.Node.Edits(text_edits)))
   13.59 +        case Edit_Node(name, master_dir, header, text_edits) if prover.isDefined =>
   13.60 +          handle_edits(name, master_dir, header, List(Document.Node.Edits(text_edits)))
   13.61            reply(())
   13.62  
   13.63          case change: Change_Node if prover.isDefined =>
   13.64 @@ -360,9 +364,9 @@
   13.65  
   13.66    def interrupt() { session_actor ! Interrupt }
   13.67  
   13.68 -  def init_node(name: String, header: Document.Node.Header, text: String)
   13.69 -  { session_actor !? Init_Node(name, header, text) }
   13.70 +  def init_node(name: String, master_dir: String, header: Document.Node_Header, text: String)
   13.71 +  { session_actor !? Init_Node(name, master_dir, header, text) }
   13.72  
   13.73 -  def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
   13.74 -  { session_actor !? Edit_Node(name, header, edits) }
   13.75 +  def edit_node(name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
   13.76 +  { session_actor !? Edit_Node(name, master_dir, header, edits) }
   13.77  }
    14.1 --- a/src/Pure/Thy/thy_header.scala	Sat Aug 13 07:56:55 2011 -0700
    14.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Aug 13 21:28:01 2011 +0200
    14.3 @@ -28,10 +28,10 @@
    14.4  
    14.5    /* theory file name */
    14.6  
    14.7 -  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    14.8 +  private val Thy_Name = new Regex("""(.*?)([^/\\:]+)\.thy""")
    14.9  
   14.10 -  def thy_name(s: String): Option[String] =
   14.11 -    s match { case Thy_Name(name) => Some(name) case _ => None }
   14.12 +  def thy_name(s: String): Option[(String, String)] =
   14.13 +    s match { case Thy_Name(prefix, name) => Some((prefix, name)) case _ => None }
   14.14  
   14.15    def thy_path(name: String): Path = Path.basic(name).ext("thy")
   14.16  
   14.17 @@ -44,7 +44,8 @@
   14.18      val theory_name = atom("theory name", _.is_name)
   14.19  
   14.20      val file =
   14.21 -      keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name
   14.22 +      keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
   14.23 +      file_name ^^ (x => (x, true))
   14.24  
   14.25      val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }
   14.26  
   14.27 @@ -106,12 +107,13 @@
   14.28  }
   14.29  
   14.30  
   14.31 -sealed case class Thy_Header(val name: String, val imports: List[String], val uses: List[String])
   14.32 +sealed case class Thy_Header(
   14.33 +  val name: String, val imports: List[String], val uses: List[(String, Boolean)])
   14.34  {
   14.35    def map(f: String => String): Thy_Header =
   14.36 -    Thy_Header(f(name), imports.map(f), uses.map(f))
   14.37 +    Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
   14.38  
   14.39    def norm_deps(f: String => String): Thy_Header =
   14.40 -    copy(imports = imports.map(name => f(name) + ".thy"), uses = uses.map(f))
   14.41 +    copy(imports = imports.map(name => f(name)), uses = uses.map(p => (f(p._1), p._2)))
   14.42  }
   14.43  
    15.1 --- a/src/Pure/Thy/thy_info.ML	Sat Aug 13 07:56:55 2011 -0700
    15.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Aug 13 21:28:01 2011 +0200
    15.3 @@ -21,8 +21,7 @@
    15.4    val use_thys_wrt: Path.T -> string list -> unit
    15.5    val use_thys: string list -> unit
    15.6    val use_thy: string -> unit
    15.7 -  val toplevel_begin_theory: Path.T option -> string ->
    15.8 -    string list -> (Path.T * bool) list -> theory
    15.9 +  val toplevel_begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> theory
   15.10    val register_thy: theory -> unit
   15.11    val finish: unit -> unit
   15.12  end;
   15.13 @@ -312,9 +311,8 @@
   15.14  
   15.15  (* toplevel begin theory -- without maintaining database *)
   15.16  
   15.17 -fun toplevel_begin_theory master name imports uses =
   15.18 +fun toplevel_begin_theory dir name imports uses =
   15.19    let
   15.20 -    val dir = (case master of SOME dir => dir | NONE => Thy_Load.get_master_path ());
   15.21      val _ = kill_thy name;
   15.22      val _ = use_thys_wrt dir imports;
   15.23      val parents = map (get_theory o base_name) imports;
    16.1 --- a/src/Pure/Thy/thy_load.ML	Sat Aug 13 07:56:55 2011 -0700
    16.2 +++ b/src/Pure/Thy/thy_load.ML	Sat Aug 13 21:28:01 2011 +0200
    16.3 @@ -167,7 +167,7 @@
    16.4      val time = ! Toplevel.timing;
    16.5  
    16.6      val _ = Present.init_theory name;
    16.7 -    fun init _ =
    16.8 +    fun init () =
    16.9        begin_theory dir name imports uses parents
   16.10        |> Present.begin_theory update_time dir uses;
   16.11  
    17.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 07:56:55 2011 -0700
    17.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 21:28:01 2011 +0200
    17.3 @@ -179,8 +179,8 @@
    17.4        var nodes = previous.nodes
    17.5  
    17.6        edits foreach {
    17.7 -        case (name, Document.Node.Remove()) =>
    17.8 -          doc_edits += (name -> Document.Node.Remove())
    17.9 +        case (name, Document.Node.Clear()) =>
   17.10 +          doc_edits += (name -> Document.Node.Clear())
   17.11            nodes -= name
   17.12  
   17.13          case (name, Document.Node.Edits(text_edits)) =>
   17.14 @@ -199,15 +199,17 @@
   17.15            doc_edits += (name -> Document.Node.Edits(cmd_edits))
   17.16            nodes += (name -> node.copy(commands = commands2))
   17.17  
   17.18 -        case (name, Document.Node.Update_Header(header)) =>
   17.19 +        case (name, Document.Node.Header(header)) =>
   17.20            val node = nodes(name)
   17.21            val update_header =
   17.22 -            (node.header.thy_header, header) match {
   17.23 -              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header))) =>
   17.24 -                thy_header0 != thy_header
   17.25 +            (node.header, header) match {
   17.26 +              case (Exn.Res(thy_header0), Exn.Res(thy_header)) => thy_header0 != thy_header
   17.27                case _ => true
   17.28              }
   17.29 -          if (update_header) doc_edits += (name -> Document.Node.Update_Header(header))
   17.30 +          if (update_header) {
   17.31 +            doc_edits += (name -> Document.Node.Header(header))
   17.32 +            nodes += (name -> node.copy(header = header))
   17.33 +          }
   17.34        }
   17.35        (doc_edits.toList, Document.Version(Document.new_id(), nodes))
   17.36      }
    18.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Aug 13 07:56:55 2011 -0700
    18.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Aug 13 21:28:01 2011 +0200
    18.3 @@ -62,9 +62,8 @@
    18.4  {
    18.5    /* pending text edits */
    18.6  
    18.7 -  def node_header(): Document.Node.Header =
    18.8 -    Document.Node.Header(master_dir,
    18.9 -      Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
   18.10 +  def node_header(): Exn.Result[Thy_Header] =
   18.11 +    Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
   18.12  
   18.13    private object pending_edits  // owned by Swing thread
   18.14    {
   18.15 @@ -78,14 +77,14 @@
   18.16          case Nil =>
   18.17          case edits =>
   18.18            pending.clear
   18.19 -          session.edit_node(node_name, node_header(), edits)
   18.20 +          session.edit_node(node_name, master_dir, node_header(), edits)
   18.21        }
   18.22      }
   18.23  
   18.24      def init()
   18.25      {
   18.26        flush()
   18.27 -      session.init_node(node_name, node_header(), Isabelle.buffer_text(buffer))
   18.28 +      session.init_node(node_name, master_dir, node_header(), Isabelle.buffer_text(buffer))
   18.29      }
   18.30  
   18.31      private val delay_flush =
    19.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 13 07:56:55 2011 -0700
    19.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 13 21:28:01 2011 +0200
    19.3 @@ -165,7 +165,7 @@
    19.4  
    19.5    val tooltip: Markup_Tree.Select[String] =
    19.6    {
    19.7 -    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
    19.8 +    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
    19.9      case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
   19.10        Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
   19.11          margin = Isabelle.Int_Property("tooltip-margin"))
    20.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Aug 13 07:56:55 2011 -0700
    20.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Aug 13 21:28:01 2011 +0200
    20.3 @@ -167,7 +167,7 @@
    20.4                new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
    20.5                  override def getShortString: String = content
    20.6                  override def getLongString: String = info_text
    20.7 -                override def toString = "\"" + content + "\" " + range.toString
    20.8 +                override def toString = quote(content) + " " + range.toString
    20.9                })
   20.10            })
   20.11      }
    21.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Aug 13 07:56:55 2011 -0700
    21.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Aug 13 21:28:01 2011 +0200
    21.3 @@ -210,8 +210,8 @@
    21.4            case None =>
    21.5              val (master_dir, path) = buffer_path(buffer)
    21.6              Thy_Header.thy_name(path) match {
    21.7 -              case Some(name) =>
    21.8 -                Some(Document_Model.init(session, buffer, master_dir, path, name))
    21.9 +              case Some((prefix, name)) =>
   21.10 +                Some(Document_Model.init(session, buffer, master_dir, prefix + name, name))
   21.11                case None => None
   21.12              }
   21.13          }
   21.14 @@ -327,13 +327,17 @@
   21.15  
   21.16    private val file_store = new Session.File_Store
   21.17    {
   21.18 -    def append(master_dir: String, path: Path): String =
   21.19 +    def append(master_dir: String, source_path: Path): String =
   21.20      {
   21.21 -      val vfs = VFSManager.getVFSForPath(master_dir)
   21.22 -      if (vfs.isInstanceOf[FileVFS])
   21.23 -        MiscUtilities.resolveSymlinks(
   21.24 -          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
   21.25 -      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
   21.26 +      val path = source_path.expand
   21.27 +      if (path.is_absolute) Isabelle_System.platform_path(path)
   21.28 +      else {
   21.29 +        val vfs = VFSManager.getVFSForPath(master_dir)
   21.30 +        if (vfs.isInstanceOf[FileVFS])
   21.31 +          MiscUtilities.resolveSymlinks(
   21.32 +            vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
   21.33 +        else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
   21.34 +      }
   21.35      }
   21.36  
   21.37      def require(canonical_name: String)