simplified/refined document model: collection of named nodes, without proper dependencies yet;
authorwenzelm
Thu Aug 05 14:35:35 2010 +0200 (2010-08-05 ago)
changeset 3815067fc24df3721
parent 38149 3c380380beac
child 38151 2837c952ca31
simplified/refined document model: collection of named nodes, without proper dependencies yet;
moved basic type definitions for ids and edits from Isar_Document to Document;
removed begin_document/end_document for now -- nodes emerge via edits;
edits refer to named nodes explicitly;
src/Pure/IsaMakefile
src/Pure/Isar/isar_document.ML
src/Pure/Isar/isar_document.scala
src/Pure/PIDE/change.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/ROOT.ML
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/document_view.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
     1.1 --- a/src/Pure/IsaMakefile	Thu Aug 05 13:41:00 2010 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Thu Aug 05 14:35:35 2010 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4    ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML		\
     1.5    ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML		\
     1.6    ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML	\
     1.7 -  ML-Systems/use_context.ML Proof/extraction.ML				\
     1.8 +  ML-Systems/use_context.ML Proof/extraction.ML PIDE/document.ML	\
     1.9    Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
    1.10    Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML	\
    1.11    ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML		\
     2.1 --- a/src/Pure/Isar/isar_document.ML	Thu Aug 05 13:41:00 2010 +0200
     2.2 +++ b/src/Pure/Isar/isar_document.ML	Thu Aug 05 14:35:35 2010 +0200
     2.3 @@ -1,7 +1,11 @@
     2.4  (*  Title:      Pure/Isar/isar_document.ML
     2.5      Author:     Makarius
     2.6  
     2.7 -Interactive Isar documents.
     2.8 +Interactive Isar documents, which are structured as follows:
     2.9 +
    2.10 +  - history: tree of documents (i.e. changes without merge)
    2.11 +  - document: graph of nodes (cf. theory files)
    2.12 +  - node: linear set of commands, potentially with proof structure
    2.13  *)
    2.14  
    2.15  structure Isar_Document: sig end =
    2.16 @@ -9,12 +13,6 @@
    2.17  
    2.18  (* unique identifiers *)
    2.19  
    2.20 -type state_id = string;
    2.21 -type command_id = string;
    2.22 -type document_id = string;
    2.23 -
    2.24 -val no_id = "";
    2.25 -
    2.26  local
    2.27    val id_count = Synchronized.var "id" 0;
    2.28  in
    2.29 @@ -32,78 +30,84 @@
    2.30  
    2.31  (** documents **)
    2.32  
    2.33 +datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option};
    2.34 +type node = entry Symtab.table; (*unique command entries indexed by command_id, start with no_id*)
    2.35 +type document = node Graph.T;   (*development graph via static imports*)
    2.36 +
    2.37 +
    2.38  (* command entries *)
    2.39  
    2.40 -datatype entry = Entry of {next: command_id option, state: state_id option};
    2.41  fun make_entry next state = Entry {next = next, state = state};
    2.42  
    2.43 -fun the_entry entries (id: command_id) =
    2.44 -  (case Symtab.lookup entries id of
    2.45 -    NONE => err_undef "document entry" id
    2.46 +fun the_entry (node: node) (id: Document.command_id) =
    2.47 +  (case Symtab.lookup node id of
    2.48 +    NONE => err_undef "command entry" id
    2.49    | SOME (Entry entry) => entry);
    2.50  
    2.51 -fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);
    2.52 +fun put_entry (id: Document.command_id, entry: entry) = Symtab.update (id, entry);
    2.53  
    2.54 -fun put_entry_state (id: command_id) state entries =
    2.55 -  let val {next, ...} = the_entry entries id
    2.56 -  in put_entry (id, make_entry next state) entries end;
    2.57 +fun put_entry_state (id: Document.command_id) state (node: node) =
    2.58 +  let val {next, ...} = the_entry node id
    2.59 +  in put_entry (id, make_entry next state) node end;
    2.60  
    2.61  fun reset_entry_state id = put_entry_state id NONE;
    2.62  fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
    2.63  
    2.64  
    2.65 -(* document *)
    2.66 -
    2.67 -datatype document = Document of
    2.68 - {dir: Path.T,                   (*master directory*)
    2.69 -  name: string,                  (*theory name*)
    2.70 -  entries: entry Symtab.table};  (*unique command entries indexed by command_id, start with no_id*)
    2.71 -
    2.72 -fun make_document dir name entries =
    2.73 -  Document {dir = dir, name = name, entries = entries};
    2.74 -
    2.75 -fun map_entries f (Document {dir, name, entries}) =
    2.76 -  make_document dir name (f entries);
    2.77 -
    2.78 -
    2.79  (* iterate entries *)
    2.80  
    2.81 -fun fold_entries id0 f (Document {entries, ...}) =
    2.82 +fun fold_entries id0 f (node: node) =
    2.83    let
    2.84      fun apply NONE x = x
    2.85        | apply (SOME id) x =
    2.86 -          let val entry = the_entry entries id
    2.87 +          let val entry = the_entry node id
    2.88            in apply (#next entry) (f (id, entry) x) end;
    2.89 -  in if Symtab.defined entries id0 then apply (SOME id0) else I end;
    2.90 +  in if Symtab.defined node id0 then apply (SOME id0) else I end;
    2.91  
    2.92 -fun first_entry P (Document {entries, ...}) =
    2.93 +fun first_entry P (node: node) =
    2.94    let
    2.95      fun first _ NONE = NONE
    2.96        | first prev (SOME id) =
    2.97 -          let val entry = the_entry entries id
    2.98 +          let val entry = the_entry node id
    2.99            in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
   2.100 -  in first NONE (SOME no_id) end;
   2.101 +  in first NONE (SOME Document.no_id) end;
   2.102  
   2.103  
   2.104  (* modify entries *)
   2.105  
   2.106 -fun insert_after (id: command_id) (id2: command_id) = map_entries (fn entries =>
   2.107 -  let val {next, state} = the_entry entries id in
   2.108 -    entries
   2.109 +fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) =
   2.110 +  let val {next, state} = the_entry node id in
   2.111 +    node
   2.112      |> put_entry (id, make_entry (SOME id2) state)
   2.113      |> put_entry (id2, make_entry next NONE)
   2.114 -  end);
   2.115 +  end;
   2.116  
   2.117 -fun delete_after (id: command_id) = map_entries (fn entries =>
   2.118 -  let val {next, state} = the_entry entries id in
   2.119 +fun delete_after (id: Document.command_id) (node: node) =
   2.120 +  let val {next, state} = the_entry node id in
   2.121      (case next of
   2.122        NONE => error ("No next entry to delete: " ^ quote id)
   2.123      | SOME id2 =>
   2.124 -        entries |>
   2.125 -          (case #next (the_entry entries id2) of
   2.126 +        node |>
   2.127 +          (case #next (the_entry node id2) of
   2.128              NONE => put_entry (id, make_entry NONE state)
   2.129            | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
   2.130 -  end);
   2.131 +  end;
   2.132 +
   2.133 +
   2.134 +(* node operations *)
   2.135 +
   2.136 +val empty_node: node = Symtab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
   2.137 +
   2.138 +fun the_node (document: document) name =
   2.139 +  Graph.get_node document name handle Graph.UNDEF _ => empty_node;
   2.140 +
   2.141 +fun edit_node (id, SOME id2) = insert_after id id2
   2.142 +  | edit_node (id, NONE) = delete_after id;
   2.143 +
   2.144 +fun edit_nodes (name, NONE) = Graph.del_node name
   2.145 +  | edit_nodes (name, SOME edits) =
   2.146 +      Graph.default_node (name, empty_node) #>
   2.147 +      Graph.map_node name (fold edit_node edits);
   2.148  
   2.149  
   2.150  
   2.151 @@ -113,16 +117,17 @@
   2.152  
   2.153  local
   2.154  
   2.155 -val global_states = Unsynchronized.ref (Symtab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))]);
   2.156 +val global_states =
   2.157 +  Unsynchronized.ref (Symtab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
   2.158  
   2.159  in
   2.160  
   2.161 -fun define_state (id: state_id) state =
   2.162 +fun define_state (id: Document.state_id) state =
   2.163    NAMED_CRITICAL "Isar" (fn () =>
   2.164      Unsynchronized.change global_states (Symtab.update_new (id, state))
   2.165        handle Symtab.DUP dup => err_dup "state" dup);
   2.166  
   2.167 -fun the_state (id: state_id) =
   2.168 +fun the_state (id: Document.state_id) =
   2.169    (case Symtab.lookup (! global_states) id of
   2.170      NONE => err_undef "state" id
   2.171    | SOME state => state);
   2.172 @@ -134,16 +139,16 @@
   2.173  
   2.174  local
   2.175  
   2.176 -val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
   2.177 +val global_commands = Unsynchronized.ref (Symtab.make [(Document.no_id, Toplevel.empty)]);
   2.178  
   2.179  in
   2.180  
   2.181 -fun define_command (id: command_id) tr =
   2.182 +fun define_command (id: Document.command_id) tr =
   2.183    NAMED_CRITICAL "Isar" (fn () =>
   2.184      Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
   2.185        handle Symtab.DUP dup => err_dup "command" dup);
   2.186  
   2.187 -fun the_command (id: command_id) =
   2.188 +fun the_command (id: Document.command_id) =
   2.189    (case Symtab.lookup (! global_commands) id of
   2.190      NONE => err_undef "command" id
   2.191    | SOME tr => tr);
   2.192 @@ -151,20 +156,20 @@
   2.193  end;
   2.194  
   2.195  
   2.196 -(* documents *)
   2.197 +(* document versions *)
   2.198  
   2.199  local
   2.200  
   2.201 -val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
   2.202 +val global_documents = Unsynchronized.ref (Symtab.make [(Document.no_id, Graph.empty: document)]);
   2.203  
   2.204  in
   2.205  
   2.206 -fun define_document (id: document_id) document =
   2.207 +fun define_document (id: Document.version_id) document =
   2.208    NAMED_CRITICAL "Isar" (fn () =>
   2.209      Unsynchronized.change global_documents (Symtab.update_new (id, document))
   2.210        handle Symtab.DUP dup => err_dup "document" dup);
   2.211  
   2.212 -fun the_document (id: document_id) =
   2.213 +fun the_document (id: Document.version_id) =
   2.214    (case Symtab.lookup (! global_documents) id of
   2.215      NONE => err_undef "document" id
   2.216    | SOME document => document);
   2.217 @@ -175,41 +180,47 @@
   2.218  
   2.219  (** main operations **)
   2.220  
   2.221 -(* begin/end document *)
   2.222 -
   2.223 -val no_entries = Symtab.make [(no_id, make_entry NONE (SOME no_id))];
   2.224 -
   2.225 -fun begin_document (id: document_id) path =
   2.226 -  let
   2.227 -    val (dir, name) = Thy_Header.split_thy_path path;
   2.228 -    val _ = define_document id (make_document dir name no_entries);
   2.229 -  in () end;
   2.230 -
   2.231 -fun end_document (id: document_id) =
   2.232 -  NAMED_CRITICAL "Isar" (fn () =>
   2.233 -    let
   2.234 -      val document as Document {name, ...} = the_document id;
   2.235 -      val end_state =
   2.236 -        the_state (the (#state (#3 (the
   2.237 -          (first_entry (fn (_, {next, ...}) => is_none next) document)))));
   2.238 -      val _ =  (* FIXME regular execution (??), result (??) *)
   2.239 -        Future.fork (fn () =>
   2.240 -          (case Lazy.force end_state of
   2.241 -            SOME st => Toplevel.end_theory (Position.id_only id) st
   2.242 -          | NONE => error ("Failed to finish theory " ^ quote name)));
   2.243 -    in () end);
   2.244 -
   2.245 -
   2.246 -(* document editing *)
   2.247 +(* execution *)
   2.248  
   2.249  local
   2.250  
   2.251 -fun is_changed entries' (id, {next = _, state}) =
   2.252 -  (case try (the_entry entries') id of
   2.253 +val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
   2.254 +
   2.255 +fun force_state NONE = ()
   2.256 +  | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));
   2.257 +
   2.258 +in
   2.259 +
   2.260 +fun execute document =
   2.261 +  NAMED_CRITICAL "Isar" (fn () =>
   2.262 +    let
   2.263 +      val old_execution = ! execution;
   2.264 +      val _ = List.app Future.cancel old_execution;
   2.265 +      fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
   2.266 +      (* FIXME proper node deps *)
   2.267 +      val new_execution = Graph.keys document |> map (fn name =>
   2.268 +        Future.fork_pri 1 (fn () =>
   2.269 +          let
   2.270 +            val _ = await_cancellation ();
   2.271 +            val exec =
   2.272 +              fold_entries Document.no_id (fn (_, {state, ...}) => fn () => force_state state)
   2.273 +                (the_node document name);
   2.274 +          in exec () end));
   2.275 +    in execution := new_execution end);
   2.276 +
   2.277 +end;
   2.278 +
   2.279 +
   2.280 +(* editing *)
   2.281 +
   2.282 +local
   2.283 +
   2.284 +fun is_changed node' (id, {next = _, state}) =
   2.285 +  (case try (the_entry node') id of
   2.286      NONE => true
   2.287    | SOME {next = _, state = state'} => state' <> state);
   2.288  
   2.289 -fun new_state name (id: command_id) (state_id, updates) =
   2.290 +fun new_state name (id: Document.command_id) (state_id, updates) =
   2.291    let
   2.292      val state = the_state state_id;
   2.293      val state_id' = create_id ();
   2.294 @@ -227,46 +238,33 @@
   2.295    |> Markup.markup Markup.assign
   2.296    |> Output.status;
   2.297  
   2.298 -
   2.299 -fun force_state NONE = ()
   2.300 -  | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));
   2.301 -
   2.302 -val execution = Unsynchronized.ref (Future.value ());
   2.303 -
   2.304 -fun execute document =
   2.305 -  NAMED_CRITICAL "Isar" (fn () =>
   2.306 -    let
   2.307 -      val old_execution = ! execution;
   2.308 -      val _ = Future.cancel old_execution;
   2.309 -      val new_execution = Future.fork_pri 1 (fn () =>
   2.310 -       (uninterruptible (K Future.join_result) old_execution;
   2.311 -        fold_entries no_id (fn (_, {state, ...}) => fn () => force_state state) document ()));
   2.312 -    in execution := new_execution end);
   2.313 -
   2.314  in
   2.315  
   2.316 -fun edit_document (old_id: document_id) (new_id: document_id) edits =
   2.317 -  NAMED_CRITICAL "Isar" (fn () =>
   2.318 +fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
   2.319 +  NAMED_CRITICAL "Isar" (fn () => exception_trace (fn () =>
   2.320      let
   2.321 -      val old_document as Document {name, entries = old_entries, ...} = the_document old_id;
   2.322 -      val new_document as Document {entries = new_entries, ...} = old_document
   2.323 -        |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
   2.324 +      val old_document = the_document old_id;
   2.325 +      val new_document = fold edit_nodes edits old_document;
   2.326  
   2.327 -      val (updates, new_document') =
   2.328 -        (case first_entry (is_changed old_entries) new_document of
   2.329 -          NONE => ([], new_document)
   2.330 +      fun update_node name node =
   2.331 +        (case first_entry (is_changed (the_node old_document name)) node of
   2.332 +          NONE => ([], node)
   2.333          | SOME (prev, id, _) =>
   2.334              let
   2.335 -              val prev_state_id = the (#state (the_entry new_entries (the prev)));
   2.336 -              val (_, updates) =
   2.337 -                fold_entries id (new_state name o #1) new_document (prev_state_id, []);
   2.338 -              val new_document' = new_document |> map_entries (fold set_entry_state updates);
   2.339 -            in (rev updates, new_document') end);
   2.340 +              val prev_state_id = the (#state (the_entry node (the prev)));
   2.341 +              val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []);
   2.342 +              val node' = fold set_entry_state updates node;
   2.343 +            in (rev updates, node') end);
   2.344 +
   2.345 +      (* FIXME proper node deps *)
   2.346 +      val (updatess, new_document') =
   2.347 +        (Graph.keys new_document, new_document)
   2.348 +          |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
   2.349  
   2.350        val _ = define_document new_id new_document';
   2.351 -      val _ = report_updates updates;
   2.352 +      val _ = report_updates (flat updatess);
   2.353        val _ = execute new_document';
   2.354 -    in () end);
   2.355 +    in () end));
   2.356  
   2.357  end;
   2.358  
   2.359 @@ -282,21 +280,13 @@
   2.360          define_command id (Outer_Syntax.prepare_command (Position.id id) text))));
   2.361  
   2.362  val _ =
   2.363 -  Outer_Syntax.internal_command "Isar.begin_document"
   2.364 -    (Parse.string -- Parse.string >> (fn (id, path) =>
   2.365 -      Toplevel.imperative (fn () => begin_document id (Path.explode path))));
   2.366 -
   2.367 -val _ =
   2.368 -  Outer_Syntax.internal_command "Isar.end_document"
   2.369 -    (Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
   2.370 -
   2.371 -val _ =
   2.372    Outer_Syntax.internal_command "Isar.edit_document"
   2.373      (Parse.string -- Parse.string --
   2.374 -        Parse_Value.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
   2.375 -      >> (fn ((id, new_id), edits) =>
   2.376 -        Toplevel.position (Position.id_only new_id) o
   2.377 -        Toplevel.imperative (fn () => edit_document id new_id edits)));
   2.378 +      Parse_Value.list
   2.379 +        (Parse.string -- Scan.option (Parse_Value.list (Parse.string -- Scan.option Parse.string)))
   2.380 +      >> (fn ((old_id, new_id), edits) =>
   2.381 +          Toplevel.position (Position.id_only new_id) o
   2.382 +          Toplevel.imperative (fn () => edit_document old_id new_id edits)));
   2.383  
   2.384  end;
   2.385  
     3.1 --- a/src/Pure/Isar/isar_document.scala	Thu Aug 05 13:41:00 2010 +0200
     3.2 +++ b/src/Pure/Isar/isar_document.scala	Thu Aug 05 14:35:35 2010 +0200
     3.3 @@ -9,13 +9,6 @@
     3.4  
     3.5  object Isar_Document
     3.6  {
     3.7 -  /* unique identifiers */
     3.8 -
     3.9 -  type State_ID = String
    3.10 -  type Command_ID = String
    3.11 -  type Document_ID = String
    3.12 -
    3.13 -
    3.14    /* reports */
    3.15  
    3.16    object Assign {
    3.17 @@ -27,7 +20,7 @@
    3.18    }
    3.19  
    3.20    object Edit {
    3.21 -    def unapply(msg: XML.Tree): Option[(Command_ID, State_ID)] =
    3.22 +    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
    3.23        msg match {
    3.24          case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
    3.25            Some(cmd_id, state_id)
    3.26 @@ -44,7 +37,7 @@
    3.27  
    3.28    /* commands */
    3.29  
    3.30 -  def define_command(id: Command_ID, text: String) {
    3.31 +  def define_command(id: Document.Command_ID, text: String) {
    3.32      output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
    3.33        Isabelle_Syntax.encode_string(text))
    3.34    }
    3.35 @@ -52,36 +45,41 @@
    3.36  
    3.37    /* documents */
    3.38  
    3.39 -  def begin_document(id: Document_ID, path: String) {
    3.40 -    output_sync("Isar.begin_document " + Isabelle_Syntax.encode_string(id) + " " +
    3.41 -      Isabelle_Syntax.encode_string(path))
    3.42 -  }
    3.43 -
    3.44 -  def end_document(id: Document_ID) {
    3.45 -    output_sync("Isar.end_document " + Isabelle_Syntax.encode_string(id))
    3.46 -  }
    3.47 -
    3.48 -  def edit_document(old_id: Document_ID, new_id: Document_ID,
    3.49 -      edits: List[(Command_ID, Option[Command_ID])])
    3.50 +  def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
    3.51 +      edits: List[Document.Edit[Document.Command_ID]])
    3.52    {
    3.53 -    def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
    3.54 +    def append_edit(
    3.55 +        edit: (Option[Document.Command_ID], Option[Document.Command_ID]), result: StringBuilder)
    3.56      {
    3.57 -      edit match {
    3.58 -        case (id, None) => Isabelle_Syntax.append_string(id, result)
    3.59 -        case (id, Some(id2)) =>
    3.60 -          Isabelle_Syntax.append_string(id, result)
    3.61 +      Isabelle_Syntax.append_string(edit._1 getOrElse Document.NO_ID, result)
    3.62 +      edit._2 match {
    3.63 +        case None =>
    3.64 +        case Some(id2) =>
    3.65            result.append(" ")
    3.66            Isabelle_Syntax.append_string(id2, result)
    3.67        }
    3.68      }
    3.69  
    3.70 +    def append_node_edit(
    3.71 +        edit: (String, Option[List[(Option[Document.Command_ID], Option[Document.Command_ID])]]),
    3.72 +        result: StringBuilder)
    3.73 +    {
    3.74 +      Isabelle_Syntax.append_string(edit._1, result)
    3.75 +      edit._2 match {
    3.76 +        case None =>
    3.77 +        case Some(eds) =>
    3.78 +          result.append(" ")
    3.79 +          Isabelle_Syntax.append_list(append_edit, eds, result)
    3.80 +      }
    3.81 +    }
    3.82 +
    3.83      val buf = new StringBuilder(40)
    3.84      buf.append("Isar.edit_document ")
    3.85      Isabelle_Syntax.append_string(old_id, buf)
    3.86      buf.append(" ")
    3.87      Isabelle_Syntax.append_string(new_id, buf)
    3.88      buf.append(" ")
    3.89 -    Isabelle_Syntax.append_list(append_edit, edits, buf)
    3.90 +    Isabelle_Syntax.append_list(append_node_edit, edits, buf)
    3.91      output_sync(buf.toString)
    3.92    }
    3.93  }
     4.1 --- a/src/Pure/PIDE/change.scala	Thu Aug 05 13:41:00 2010 +0200
     4.2 +++ b/src/Pure/PIDE/change.scala	Thu Aug 05 14:35:35 2010 +0200
     4.3 @@ -8,11 +8,16 @@
     4.4  package isabelle
     4.5  
     4.6  
     4.7 +object Change
     4.8 +{
     4.9 +  val init = new Change(Document.NO_ID, None, Nil, Future.value(Nil, Document.init))
    4.10 +}
    4.11 +
    4.12  class Change(
    4.13 -  val id: Isar_Document.Document_ID,
    4.14 +  val id: Document.Version_ID,
    4.15    val parent: Option[Change],
    4.16 -  val edits: List[Text_Edit],
    4.17 -  val result: Future[(List[Document.Edit], Document)])
    4.18 +  val edits: List[Document.Node.Text_Edit],
    4.19 +  val result: Future[(List[Document.Edit[Command]], Document)])
    4.20  {
    4.21    def ancestors: Iterator[Change] = new Iterator[Change]
    4.22    {
    4.23 @@ -28,10 +33,10 @@
    4.24    def join_document: Document = result.join._2
    4.25    def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
    4.26  
    4.27 -  def edit(session: Session, edits: List[Text_Edit]): Change =
    4.28 +  def edit(session: Session, edits: List[Document.Node.Text_Edit]): Change =
    4.29    {
    4.30      val new_id = session.create_id()
    4.31 -    val result: Future[(List[Document.Edit], Document)] =
    4.32 +    val result: Future[(List[Document.Edit[Command]], Document)] =
    4.33        Future.fork {
    4.34          val old_doc = join_document
    4.35          old_doc.await_assignment
     5.1 --- a/src/Pure/PIDE/command.scala	Thu Aug 05 13:41:00 2010 +0200
     5.2 +++ b/src/Pure/PIDE/command.scala	Thu Aug 05 14:35:35 2010 +0200
     5.3 @@ -35,7 +35,7 @@
     5.4  }
     5.5  
     5.6  class Command(
     5.7 -    val id: Isar_Document.Command_ID,
     5.8 +    val id: Document.Command_ID,
     5.9      val span: Thy_Syntax.Span,
    5.10      val static_parent: Option[Command] = None)
    5.11    extends Session.Entity
    5.12 @@ -91,7 +91,7 @@
    5.13      accumulator ! Consume(message, forward)
    5.14    }
    5.15  
    5.16 -  def assign_state(state_id: Isar_Document.State_ID): Command =
    5.17 +  def assign_state(state_id: Document.State_ID): Command =
    5.18    {
    5.19      val cmd = new Command(state_id, span, Some(this))
    5.20      accumulator !? Assign
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 05 14:35:35 2010 +0200
     6.3 @@ -0,0 +1,36 @@
     6.4 +(*  Title:      Pure/PIDE/document.ML
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Document as collection of named nodes, each consisting of an editable
     6.8 +list of commands.
     6.9 +*)
    6.10 +
    6.11 +signature DOCUMENT =
    6.12 +sig
    6.13 +  type state_id = string
    6.14 +  type command_id = string
    6.15 +  type version_id = string
    6.16 +  val no_id: string
    6.17 +  type edit = string * ((command_id * command_id option) list) option
    6.18 +end;
    6.19 +
    6.20 +structure Document: DOCUMENT =
    6.21 +struct
    6.22 +
    6.23 +(* unique identifiers *)
    6.24 +
    6.25 +type state_id = string;
    6.26 +type command_id = string;
    6.27 +type version_id = string;
    6.28 +
    6.29 +val no_id = "";
    6.30 +
    6.31 +
    6.32 +(* edits *)
    6.33 +
    6.34 +type edit =
    6.35 +  string *  (*node name*)
    6.36 +  ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
    6.37 +
    6.38 +end;
    6.39 +
     7.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 05 13:41:00 2010 +0200
     7.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 05 14:35:35 2010 +0200
     7.3 @@ -1,17 +1,37 @@
     7.4  /*  Title:      Pure/PIDE/document.scala
     7.5      Author:     Makarius
     7.6  
     7.7 -Document as editable list of commands.
     7.8 +Document as collection of named nodes, each consisting of an editable
     7.9 +list of commands.
    7.10  */
    7.11  
    7.12  package isabelle
    7.13  
    7.14  
    7.15 +import scala.collection.mutable
    7.16  import scala.annotation.tailrec
    7.17  
    7.18  
    7.19  object Document
    7.20  {
    7.21 +  /* unique identifiers */
    7.22 +
    7.23 +  type State_ID = String
    7.24 +  type Command_ID = String
    7.25 +  type Version_ID = String
    7.26 +
    7.27 +  val NO_ID = ""
    7.28 +
    7.29 +
    7.30 +  /* nodes */
    7.31 +
    7.32 +  object Node { type Text_Edit = (String, List[isabelle.Text_Edit]) }  // FIXME None: remove
    7.33 +
    7.34 +  type Edit[C] =
    7.35 +   (String,  // node name
    7.36 +    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
    7.37 +
    7.38 +
    7.39    /* command start positions */
    7.40  
    7.41    def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
    7.42 @@ -25,11 +45,11 @@
    7.43    }
    7.44  
    7.45  
    7.46 -  /* empty document */
    7.47 +  /* initial document */
    7.48  
    7.49 -  def empty(id: Isar_Document.Document_ID): Document =
    7.50 +  val init: Document =
    7.51    {
    7.52 -    val doc = new Document(id, Linear_Set(), Map())
    7.53 +    val doc = new Document(NO_ID, Map().withDefaultValue(Linear_Set()), Map())
    7.54      doc.assign_states(Nil)
    7.55      doc
    7.56    }
    7.57 @@ -38,10 +58,8 @@
    7.58  
    7.59    /** document edits **/
    7.60  
    7.61 -  type Edit = (Option[Command], Option[Command])
    7.62 -
    7.63 -  def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
    7.64 -    edits: List[Text_Edit]): (List[Edit], Document) =
    7.65 +  def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
    7.66 +      edits: List[Node.Text_Edit]): (List[Edit[Command]], Document) =
    7.67    {
    7.68      require(old_doc.assignment.is_finished)
    7.69  
    7.70 @@ -56,7 +74,8 @@
    7.71  
    7.72      /* phase 1: edit individual command source */
    7.73  
    7.74 -    def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
    7.75 +    @tailrec def edit_text(eds: List[Text_Edit],
    7.76 +        commands: Linear_Set[Command]): Linear_Set[Command] =
    7.77      {
    7.78        eds match {
    7.79          case e :: es =>
    7.80 @@ -120,51 +139,64 @@
    7.81  
    7.82      /* phase 3: resulting document edits */
    7.83  
    7.84 -    val commands0 = old_doc.commands
    7.85 -    val commands1 = edit_text(edits, commands0)
    7.86 -    val commands2 = parse_spans(commands1)
    7.87 +    {
    7.88 +      val doc_edits = new mutable.ListBuffer[Edit[Command]]
    7.89 +      var nodes = old_doc.nodes
    7.90 +      var former_states = old_doc.assignment.join
    7.91  
    7.92 -    val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
    7.93 -    val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
    7.94 +      for ((name, text_edits) <- edits) {
    7.95 +        val commands0 = nodes(name)
    7.96 +        val commands1 = edit_text(text_edits, commands0)
    7.97 +        val commands2 = parse_spans(commands1)
    7.98  
    7.99 -    val doc_edits =
   7.100 -      removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
   7.101 -      inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
   7.102 +        val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
   7.103 +        val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
   7.104 +
   7.105 +        val cmd_edits =
   7.106 +          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
   7.107 +          inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
   7.108  
   7.109 -    val former_states = old_doc.assignment.join -- removed_commands
   7.110 -
   7.111 -    (doc_edits, new Document(new_id, commands2, former_states))
   7.112 +        doc_edits += (name -> Some(cmd_edits))
   7.113 +        nodes += (name -> commands2)
   7.114 +        former_states --= removed_commands
   7.115 +      }
   7.116 +      (doc_edits.toList, new Document(new_id, nodes, former_states))
   7.117 +    }
   7.118    }
   7.119  }
   7.120  
   7.121  
   7.122  class Document(
   7.123 -    val id: Isar_Document.Document_ID,
   7.124 -    val commands: Linear_Set[Command],
   7.125 -    former_states: Map[Command, Command])
   7.126 +    val id: Document.Version_ID,
   7.127 +    val nodes: Map[String, Linear_Set[Command]],
   7.128 +    former_states: Map[Command, Command])  // FIXME !?
   7.129  {
   7.130    /* command ranges */
   7.131  
   7.132 -  def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands.iterator)
   7.133 +  def commands(name: String): Linear_Set[Command] = nodes.get(name) getOrElse Linear_Set()
   7.134  
   7.135 -  def command_start(cmd: Command): Option[Int] =
   7.136 -    command_starts.find(_._1 == cmd).map(_._2)
   7.137 +  def command_starts(name: String): Iterator[(Command, Int)] =
   7.138 +    Document.command_starts(commands(name).iterator)
   7.139 +
   7.140 +  def command_start(name: String, cmd: Command): Option[Int] =
   7.141 +    command_starts(name).find(_._1 == cmd).map(_._2)
   7.142  
   7.143 -  def command_range(i: Int): Iterator[(Command, Int)] =
   7.144 -    command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
   7.145 +  def command_range(name: String, i: Int): Iterator[(Command, Int)] =
   7.146 +    command_starts(name) dropWhile { case (cmd, start) => start + cmd.length <= i }
   7.147  
   7.148 -  def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
   7.149 -    command_range(i) takeWhile { case (_, start) => start < j }
   7.150 +  def command_range(name: String, i: Int, j: Int): Iterator[(Command, Int)] =
   7.151 +    command_range(name, i) takeWhile { case (_, start) => start < j }
   7.152  
   7.153 -  def command_at(i: Int): Option[(Command, Int)] =
   7.154 +  def command_at(name: String, i: Int): Option[(Command, Int)] =
   7.155    {
   7.156 -    val range = command_range(i)
   7.157 +    val range = command_range(name, i)
   7.158      if (range.hasNext) Some(range.next) else None
   7.159    }
   7.160  
   7.161 -  def proper_command_at(i: Int): Option[Command] =
   7.162 -    command_at(i) match {
   7.163 -      case Some((command, _)) => commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
   7.164 +  def proper_command_at(name: String, i: Int): Option[Command] =
   7.165 +    command_at(name, i) match {
   7.166 +      case Some((command, _)) =>
   7.167 +        commands(name).reverse_iterator(command).find(cmd => !cmd.is_ignored)
   7.168        case None => None
   7.169      }
   7.170  
     8.1 --- a/src/Pure/ROOT.ML	Thu Aug 05 13:41:00 2010 +0200
     8.2 +++ b/src/Pure/ROOT.ML	Thu Aug 05 14:35:35 2010 +0200
     8.3 @@ -234,6 +234,7 @@
     8.4  use "Thy/term_style.ML";
     8.5  use "Thy/thy_output.ML";
     8.6  use "Thy/thy_syntax.ML";
     8.7 +use "PIDE/document.ML";
     8.8  use "old_goals.ML";
     8.9  use "Isar/outer_syntax.ML";
    8.10  use "Thy/thy_info.ML";
     9.1 --- a/src/Pure/System/session.scala	Thu Aug 05 13:41:00 2010 +0200
     9.2 +++ b/src/Pure/System/session.scala	Thu Aug 05 14:35:35 2010 +0200
     9.3 @@ -76,7 +76,6 @@
     9.4  
     9.5    private case class Start(timeout: Int, args: List[String])
     9.6    private case object Stop
     9.7 -  private case class Begin_Document(path: String)
     9.8  
     9.9    private lazy val session_actor = actor {
    9.10  
    9.11 @@ -84,8 +83,9 @@
    9.12  
    9.13      def register(entity: Session.Entity) { entities += (entity.id -> entity) }
    9.14  
    9.15 -    var documents = Map[Isar_Document.Document_ID, Document]()
    9.16 +    var documents = Map[Document.Version_ID, Document]()
    9.17      def register_document(doc: Document) { documents += (doc.id -> doc) }
    9.18 +    register_document(Document.init)
    9.19  
    9.20  
    9.21      /* document changes */
    9.22 @@ -94,22 +94,31 @@
    9.23      {
    9.24        require(change.parent.isDefined)
    9.25  
    9.26 -      val (changes, doc) = change.result.join
    9.27 -      val id_changes = changes map {
    9.28 -        case (c1, c2) =>
    9.29 -          (c1.map(_.id).getOrElse(""),
    9.30 -           c2 match {
    9.31 -              case None => None
    9.32 -              case Some(command) =>
    9.33 -                if (!lookup_command(command.id).isDefined) {
    9.34 -                  register(command)
    9.35 -                  prover.define_command(command.id, system.symbols.encode(command.source))
    9.36 -                }
    9.37 -                Some(command.id)
    9.38 -            })
    9.39 -      }
    9.40 +      val (node_edits, doc) = change.result.join
    9.41 +      val id_edits =
    9.42 +        node_edits map {
    9.43 +          case (name, None) => (name, None)
    9.44 +          case (name, Some(cmd_edits)) =>
    9.45 +            val chs =
    9.46 +              cmd_edits map {
    9.47 +                case (c1, c2) =>
    9.48 +                  val id1 = c1.map(_.id)
    9.49 +                  val id2 =
    9.50 +                    c2 match {
    9.51 +                      case None => None
    9.52 +                      case Some(command) =>
    9.53 +                        if (!lookup_command(command.id).isDefined) {
    9.54 +                          register(command)
    9.55 +                          prover.define_command(command.id, system.symbols.encode(command.source))
    9.56 +                        }
    9.57 +                        Some(command.id)
    9.58 +                    }
    9.59 +                  (id1, id2)
    9.60 +              }
    9.61 +            (name -> Some(chs))
    9.62 +        }
    9.63        register_document(doc)
    9.64 -      prover.edit_document(change.parent.get.id, doc.id, id_changes)
    9.65 +      prover.edit_document(change.parent.get.id, doc.id, id_edits)
    9.66      }
    9.67  
    9.68  
    9.69 @@ -229,13 +238,6 @@
    9.70              prover = null
    9.71            }
    9.72  
    9.73 -        case Begin_Document(path: String) if prover != null =>
    9.74 -          val id = create_id()
    9.75 -          val doc = Document.empty(id)
    9.76 -          register_document(doc)
    9.77 -          prover.begin_document(id, path)
    9.78 -          reply(doc)
    9.79 -
    9.80          case change: Change if prover != null =>
    9.81            handle_change(change)
    9.82  
    9.83 @@ -304,7 +306,4 @@
    9.84  
    9.85    def stop() { session_actor ! Stop }
    9.86    def input(change: Change) { session_actor ! change }
    9.87 -
    9.88 -  def begin_document(path: String): Document =
    9.89 -    (session_actor !? Begin_Document(path)).asInstanceOf[Document]
    9.90  }
    10.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 05 13:41:00 2010 +0200
    10.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 05 14:35:35 2010 +0200
    10.3 @@ -71,10 +71,10 @@
    10.4  
    10.5    /* history */
    10.6  
    10.7 -  private val document_0 = session.begin_document(buffer.getName)
    10.8 +  // FIXME proper error handling
    10.9 +  val thy_name = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))._2
   10.10  
   10.11 -  @volatile private var history =  // owned by Swing thread
   10.12 -    new Change(document_0.id, None, Nil, Future.value(Nil, document_0))
   10.13 +  @volatile private var history = Change.init // owned by Swing thread
   10.14  
   10.15    def current_change(): Change = history
   10.16    def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document
   10.17 @@ -86,7 +86,8 @@
   10.18    {
   10.19      Swing_Thread.assert()
   10.20      (edits_buffer.toList /:
   10.21 -      current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits)
   10.22 +      current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) =>
   10.23 +        (for ((name, eds) <- change.edits if name == thy_name) yield eds).flatten ::: edits)
   10.24    }
   10.25  
   10.26    def from_current(doc: Document, offset: Int): Int =
   10.27 @@ -102,7 +103,7 @@
   10.28  
   10.29    private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
   10.30      if (!edits_buffer.isEmpty) {
   10.31 -      val new_change = current_change().edit(session, edits_buffer.toList)
   10.32 +      val new_change = current_change().edit(session, List((thy_name, edits_buffer.toList)))
   10.33        edits_buffer.clear
   10.34        history = new_change
   10.35        new_change.result.map(_ => session.input(new_change))
    11.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 05 13:41:00 2010 +0200
    11.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 05 14:35:35 2010 +0200
    11.3 @@ -106,7 +106,7 @@
    11.4            Swing_Thread.now {
    11.5              // FIXME cover doc states as well!!?
    11.6              val document = model.recent_document()
    11.7 -            if (changed.exists(document.commands.contains))
    11.8 +            if (changed.exists(document.commands(model.thy_name).contains))
    11.9                full_repaint(document, changed)
   11.10            }
   11.11  
   11.12 @@ -122,7 +122,7 @@
   11.13      val buffer = model.buffer
   11.14      var visible_change = false
   11.15  
   11.16 -    for ((command, start) <- document.command_starts) {
   11.17 +    for ((command, start) <- document.command_starts(model.thy_name)) {
   11.18        if (changed(command)) {
   11.19          val stop = start + command.length
   11.20          val line1 = buffer.getLineOfOffset(model.to_current(document, start))
   11.21 @@ -154,11 +154,12 @@
   11.22  
   11.23          val command_range: Iterable[(Command, Int)] =
   11.24          {
   11.25 -          val range = document.command_range(from_current(start(0)))
   11.26 +          val range = document.command_range(model.thy_name, from_current(start(0)))
   11.27            if (range.hasNext) {
   11.28              val (cmd0, start0) = range.next
   11.29              new Iterable[(Command, Int)] {
   11.30 -              def iterator = Document.command_starts(document.commands.iterator(cmd0), start0)
   11.31 +              def iterator =
   11.32 +                Document.command_starts(document.commands(model.thy_name).iterator(cmd0), start0)
   11.33              }
   11.34            }
   11.35            else Iterable.empty
   11.36 @@ -197,7 +198,7 @@
   11.37      {
   11.38        val document = model.recent_document()
   11.39        val offset = model.from_current(document, text_area.xyToOffset(x, y))
   11.40 -      document.command_at(offset) match {
   11.41 +      document.command_at(model.thy_name, offset) match {
   11.42          case Some((command, command_start)) =>
   11.43            document.current_state(command).type_at(offset - command_start) match {
   11.44              case Some(text) => Isabelle.tooltip(text)
   11.45 @@ -212,7 +213,7 @@
   11.46    /* caret handling */
   11.47  
   11.48    def selected_command(): Option[Command] =
   11.49 -    model.recent_document().proper_command_at(text_area.getCaretPosition)
   11.50 +    model.recent_document().proper_command_at(model.thy_name, text_area.getCaretPosition)
   11.51  
   11.52    private val caret_listener = new CaretListener {
   11.53      private val delay = Swing_Thread.delay_last(session.input_delay) {
   11.54 @@ -266,7 +267,7 @@
   11.55        def to_current(pos: Int) = model.to_current(document, pos)
   11.56        val saved_color = gfx.getColor  // FIXME needed!?
   11.57        try {
   11.58 -        for ((command, start) <- document.command_starts if !command.is_ignored) {
   11.59 +        for ((command, start) <- document.command_starts(model.thy_name) if !command.is_ignored) {
   11.60            val line1 = buffer.getLineOfOffset(to_current(start))
   11.61            val line2 = buffer.getLineOfOffset(to_current(start + command.length)) + 1
   11.62            val y = line_to_y(line1)
    12.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Aug 05 13:41:00 2010 +0200
    12.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Aug 05 14:35:35 2010 +0200
    12.3 @@ -44,7 +44,7 @@
    12.4        case Some(model) =>
    12.5          val document = model.recent_document()
    12.6          val offset = model.from_current(document, original_offset)
    12.7 -        document.command_at(offset) match {
    12.8 +        document.command_at(model.thy_name, offset) match {
    12.9            case Some((command, command_start)) =>
   12.10              document.current_state(command).ref_at(offset - command_start) match {
   12.11                case Some(ref) =>
   12.12 @@ -57,7 +57,7 @@
   12.13                    case Command.RefInfo(_, _, Some(id), Some(offset)) =>
   12.14                      Isabelle.session.lookup_entity(id) match {
   12.15                        case Some(ref_cmd: Command) =>
   12.16 -                        document.command_start(ref_cmd) match {
   12.17 +                        document.command_start(model.thy_name, ref_cmd) match {
   12.18                            case Some(ref_cmd_start) =>
   12.19                              new Internal_Hyperlink(begin, end, line,
   12.20                                model.to_current(document, ref_cmd_start + offset - 1))
    13.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 05 13:41:00 2010 +0200
    13.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 05 14:35:35 2010 +0200
    13.3 @@ -97,7 +97,7 @@
    13.4      val root = data.root
    13.5      val document = model.recent_document()
    13.6      for {
    13.7 -      (command, command_start) <- document.command_range(0)
    13.8 +      (command, command_start) <- document.command_range(model.thy_name, 0)
    13.9        if command.is_command && !stopped
   13.10      }
   13.11      {
   13.12 @@ -129,7 +129,7 @@
   13.13  
   13.14      val root = data.root
   13.15      val document = model.recent_document()
   13.16 -    for ((command, command_start) <- document.command_range(0) if !stopped) {
   13.17 +    for ((command, command_start) <- document.command_range(model.thy_name, 0) if !stopped) {
   13.18        root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
   13.19            {
   13.20              val content = command.source(node.start, node.stop).replace('\n', ' ')
    14.1 --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Aug 05 13:41:00 2010 +0200
    14.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Aug 05 14:35:35 2010 +0200
    14.3 @@ -166,7 +166,7 @@
    14.4  
    14.5      var next_x = start
    14.6      for {
    14.7 -      (command, command_start) <- document.command_range(from(start), from(stop))
    14.8 +      (command, command_start) <- document.command_range(model.thy_name, from(start), from(stop))
    14.9        markup <- document.current_state(command).highlight.flatten
   14.10        val abs_start = to(command_start + markup.start)
   14.11        val abs_stop = to(command_start + markup.stop)