src/Pure/System/isar_document.ML
changeset 38417 b8922ae21111
parent 38414 49f1f657adc2
child 38418 9a7af64d71bb
     1.1 --- a/src/Pure/System/isar_document.ML	Sun Aug 15 13:17:45 2010 +0200
     1.2 +++ b/src/Pure/System/isar_document.ML	Sun Aug 15 14:18:52 2010 +0200
     1.3 @@ -27,11 +27,11 @@
     1.4  fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
     1.5  
     1.6  
     1.7 -(** documents **)
     1.8 +(** document versions **)
     1.9  
    1.10  datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option};
    1.11  type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
    1.12 -type document = node Graph.T;   (*development graph via static imports*)
    1.13 +type version = node Graph.T;   (*development graph via static imports*)
    1.14  
    1.15  
    1.16  (* command entries *)
    1.17 @@ -97,8 +97,8 @@
    1.18  
    1.19  val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
    1.20  
    1.21 -fun the_node (document: document) name =
    1.22 -  Graph.get_node document name handle Graph.UNDEF _ => empty_node;
    1.23 +fun the_node (version: version) name =
    1.24 +  Graph.get_node version name handle Graph.UNDEF _ => empty_node;
    1.25  
    1.26  fun edit_node (id, SOME id2) = insert_after id id2
    1.27    | edit_node (id, NONE) = delete_after id;
    1.28 @@ -166,19 +166,19 @@
    1.29  
    1.30  local
    1.31  
    1.32 -val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]);
    1.33 +val global_versions = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: version)]);
    1.34  
    1.35  in
    1.36  
    1.37 -fun define_document (id: Document.version_id) document =
    1.38 +fun define_version (id: Document.version_id) version =
    1.39    NAMED_CRITICAL "Isar" (fn () =>
    1.40 -    Unsynchronized.change global_documents (Inttab.update_new (id, document))
    1.41 -      handle Inttab.DUP dup => err_dup "document" dup);
    1.42 +    Unsynchronized.change global_versions (Inttab.update_new (id, version))
    1.43 +      handle Inttab.DUP dup => err_dup "version" dup);
    1.44  
    1.45 -fun the_document (id: Document.version_id) =
    1.46 -  (case Inttab.lookup (! global_documents) id of
    1.47 -    NONE => err_undef "document" id
    1.48 -  | SOME document => document);
    1.49 +fun the_version (id: Document.version_id) =
    1.50 +  (case Inttab.lookup (! global_versions) id of
    1.51 +    NONE => err_undef "version" id
    1.52 +  | SOME version => version);
    1.53  
    1.54  end;
    1.55  
    1.56 @@ -197,20 +197,20 @@
    1.57  
    1.58  in
    1.59  
    1.60 -fun execute document =
    1.61 +fun execute version =
    1.62    NAMED_CRITICAL "Isar" (fn () =>
    1.63      let
    1.64        val old_execution = ! execution;
    1.65        val _ = List.app Future.cancel old_execution;
    1.66        fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
    1.67        (* FIXME proper node deps *)
    1.68 -      val new_execution = Graph.keys document |> map (fn name =>
    1.69 +      val new_execution = Graph.keys version |> map (fn name =>
    1.70          Future.fork_pri 1 (fn () =>
    1.71            let
    1.72              val _ = await_cancellation ();
    1.73              val exec =
    1.74                fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
    1.75 -                (the_node document name);
    1.76 +                (the_node version name);
    1.77            in exec () end));
    1.78      in execution := new_execution end);
    1.79  
    1.80 @@ -249,11 +249,11 @@
    1.81  fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
    1.82    NAMED_CRITICAL "Isar" (fn () =>
    1.83      let
    1.84 -      val old_document = the_document old_id;
    1.85 -      val new_document = fold edit_nodes edits old_document;
    1.86 +      val old_version = the_version old_id;
    1.87 +      val new_version = fold edit_nodes edits old_version;
    1.88  
    1.89        fun update_node name node =
    1.90 -        (case first_entry (is_changed (the_node old_document name)) node of
    1.91 +        (case first_entry (is_changed (the_node old_version name)) node of
    1.92            NONE => ([], node)
    1.93          | SOME (prev, id, _) =>
    1.94              let
    1.95 @@ -263,13 +263,13 @@
    1.96              in (rev updates, node') end);
    1.97  
    1.98        (* FIXME proper node deps *)
    1.99 -      val (updatess, new_document') =
   1.100 -        (Graph.keys new_document, new_document)
   1.101 +      val (updatess, new_version') =
   1.102 +        (Graph.keys new_version, new_version)
   1.103            |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
   1.104  
   1.105 -      val _ = define_document new_id new_document';
   1.106 +      val _ = define_version new_id new_version';
   1.107        val _ = updates_status new_id (flat updatess);
   1.108 -      val _ = execute new_document';
   1.109 +      val _ = execute new_version';
   1.110      in () end);
   1.111  
   1.112  end;
   1.113 @@ -283,7 +283,7 @@
   1.114      (fn [id, text] => define_command (Document.parse_id id) text);
   1.115  
   1.116  val _ =
   1.117 -  Isabelle_Process.add_command "Isar_Document.edit_document"
   1.118 +  Isabelle_Process.add_command "Isar_Document.edit_version"
   1.119      (fn [old_id, new_id, edits] =>
   1.120        edit_document (Document.parse_id old_id) (Document.parse_id new_id)
   1.121          (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string