maintain node header;
authorwenzelm
Sat Aug 13 13:42:35 2011 +0200 (2011-08-13)
changeset 44180a6dc270d3edb
parent 44179 9411ed32f3a7
child 44181 bbce0417236d
maintain node header;
misc tuning and clarification;
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 13 12:23:51 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 13 13:42:35 2011 +0200
     1.3 @@ -15,10 +15,11 @@
     1.4    val new_id: unit -> id
     1.5    val parse_id: string -> id
     1.6    val print_id: id -> string
     1.7 +  type node_header = string * string list * string list
     1.8    datatype node_edit =
     1.9      Remove |
    1.10      Edits of (command_id option * command_id option) list |
    1.11 -    Update_Header of (string * string list * string list) Exn.result
    1.12 +    Update_Header of node_header Exn.result
    1.13    type edit = string * node_edit
    1.14    type state
    1.15    val init_state: state
    1.16 @@ -54,24 +55,33 @@
    1.17  
    1.18  (** document structure **)
    1.19  
    1.20 +type node_header = string * string list * string list;
    1.21  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    1.22  
    1.23  abstype node = Node of
    1.24 -  {last: exec_id, entries: exec_id option Entries.T}  (*command entries with excecutions*)
    1.25 + {header: node_header Exn.result,
    1.26 +  entries: exec_id option Entries.T,  (*command entries with excecutions*)
    1.27 +  last: exec_id}  (*last entry with main result*)
    1.28  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.29  with
    1.30  
    1.31 -fun make_node (last, entries) =
    1.32 -  Node {last = last, entries = entries};
    1.33 +fun make_node (header, entries, last) =
    1.34 +  Node {header = header, entries = entries, last = last};
    1.35  
    1.36 -fun get_last (Node {last, ...}) = last;
    1.37 -fun set_last last (Node {entries, ...}) = make_node (last, entries);
    1.38 +fun map_node f (Node {header, entries, last}) =
    1.39 +  make_node (f (header, entries, last));
    1.40  
    1.41 -fun map_entries f (Node {last, entries}) = make_node (last, f entries);
    1.42 +fun get_header (Node {header, ...}) = header;
    1.43 +fun set_header header = map_node (fn (_, entries, last) => (header, entries, last));
    1.44 +
    1.45 +fun map_entries f (Node {header, entries, last}) = make_node (header, f entries, last);
    1.46  fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
    1.47  fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
    1.48  
    1.49 -val empty_node = make_node (no_id, Entries.empty);
    1.50 +fun get_last (Node {last, ...}) = last;
    1.51 +fun set_last last = map_node (fn (header, entries, _) => (header, entries, last));
    1.52 +
    1.53 +val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, no_id);
    1.54  val empty_version = Version Graph.empty;
    1.55  
    1.56  
    1.57 @@ -80,7 +90,7 @@
    1.58  datatype node_edit =
    1.59    Remove |
    1.60    Edits of (command_id option * command_id option) list |
    1.61 -  Update_Header of (string * string list * string list) Exn.result;
    1.62 +  Update_Header of node_header Exn.result;
    1.63  
    1.64  type edit = string * node_edit;
    1.65  
    1.66 @@ -110,15 +120,16 @@
    1.67  fun get_node version name = Graph.get_node (nodes_of version) name
    1.68    handle Graph.UNDEF _ => empty_node;
    1.69  
    1.70 +fun update_node name f =
    1.71 +  Graph.default_node (name, empty_node) #> Graph.map_node name f;
    1.72 +
    1.73  fun edit_nodes (name, node_edit) (Version nodes) =
    1.74    Version
    1.75      (case node_edit of
    1.76        Remove => perhaps (try (Graph.del_node name)) nodes
    1.77 -    | Edits edits =>
    1.78 -        nodes
    1.79 -        |> Graph.default_node (name, empty_node)
    1.80 -        |> Graph.map_node name (edit_node edits)
    1.81 -    | Update_Header _ => nodes);  (* FIXME *)
    1.82 +    | Edits edits => update_node name (edit_node edits) nodes
    1.83 +    (* FIXME maintain deps; cycles!? *)
    1.84 +    | Update_Header header => update_node name (set_header header) nodes);
    1.85  
    1.86  fun put_node name node (Version nodes) =
    1.87    Version (nodes
    1.88 @@ -204,7 +215,10 @@
    1.89  fun get_theory state version_id pos name =
    1.90    let
    1.91      val last = get_last (get_node (the_version state version_id) name);
    1.92 -    val st = #2 (Lazy.force (the_exec state last));
    1.93 +    val st =
    1.94 +      (case Lazy.peek (the_exec state last) of
    1.95 +        SOME result => #2 (Exn.release result)
    1.96 +      | NONE => error ("Unfinished execution for theory " ^ quote name));
    1.97    in Toplevel.end_theory pos st end;
    1.98  
    1.99  
   1.100 @@ -252,7 +266,7 @@
   1.101  fun run_command node_name raw_tr st =
   1.102    (case
   1.103        (case Toplevel.init_of raw_tr of
   1.104 -        SOME name =>
   1.105 +        SOME _ =>
   1.106            Exn.capture (fn () =>
   1.107              let val master_dir = Path.dir (Path.explode node_name);  (* FIXME move to Scala side *)
   1.108              in Toplevel.modify_master (SOME master_dir) raw_tr end) ()
   1.109 @@ -320,7 +334,7 @@
   1.110  fun edit (old_id: version_id) (new_id: version_id) edits state =
   1.111    let
   1.112      val old_version = the_version state old_id;
   1.113 -    val _ = Time.now ();  (* FIXME odd workaround *)
   1.114 +    val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
   1.115      val new_version = fold edit_nodes edits old_version;
   1.116  
   1.117      fun update_node name (rev_updates, version, st) =
   1.118 @@ -360,7 +374,7 @@
   1.119        fun force_exec NONE = ()
   1.120          | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
   1.121  
   1.122 -      val execution' = (* FIXME proper node deps *)
   1.123 +      val execution' = (* FIXME Graph.schedule *)
   1.124          Future.forks
   1.125            {name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true}
   1.126            [fn () =>
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 12:23:51 2011 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 13:42:35 2011 +0200
     2.3 @@ -207,7 +207,10 @@
     2.4                  thy_header0 != thy_header
     2.5                case _ => true
     2.6              }
     2.7 -          if (update_header) doc_edits += (name -> Document.Node.Update_Header(header))
     2.8 +          if (update_header) {
     2.9 +            doc_edits += (name -> Document.Node.Update_Header(header))
    2.10 +            nodes += (name -> node.copy(header = header))
    2.11 +          }
    2.12        }
    2.13        (doc_edits.toList, Document.Version(Document.new_id(), nodes))
    2.14      }