src/Pure/PIDE/document.ML
changeset 44185 05641edb5d30
parent 44182 ecb51b457064
child 44186 806f0ec1a43d
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 13 16:07:26 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 13 20:20:36 2011 +0200
     1.3 @@ -15,9 +15,9 @@
     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) Exn.result
     1.8 +  type node_header = (string * string list * (string * bool) list) Exn.result
     1.9    datatype node_edit =
    1.10 -    Remove |
    1.11 +    Clear |
    1.12      Edits of (command_id option * command_id option) list |
    1.13      Header of node_header
    1.14    type edit = string * node_edit
    1.15 @@ -55,7 +55,7 @@
    1.16  
    1.17  (** document structure **)
    1.18  
    1.19 -type node_header = (string * string list * string list) Exn.result;
    1.20 +type node_header = (string * string list * (string * bool) list) Exn.result;
    1.21  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    1.22  
    1.23  abstype node = Node of
    1.24 @@ -82,13 +82,17 @@
    1.25  fun set_last last = map_node (fn (header, entries, _) => (header, entries, last));
    1.26  
    1.27  val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, no_id);
    1.28 -val empty_version = Version Graph.empty;
    1.29 +val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, no_id));
    1.30 +
    1.31 +fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
    1.32 +fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
    1.33 +fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f;
    1.34  
    1.35  
    1.36  (* node edits and associated executions *)
    1.37  
    1.38  datatype node_edit =
    1.39 -  Remove |
    1.40 +  Clear |
    1.41    Edits of (command_id option * command_id option) list |
    1.42    Header of node_header;
    1.43  
    1.44 @@ -114,22 +118,30 @@
    1.45  
    1.46  (* version operations *)
    1.47  
    1.48 +val empty_version = Version Graph.empty;
    1.49 +
    1.50  fun nodes_of (Version nodes) = nodes;
    1.51 +val node_of = get_node o nodes_of;
    1.52  val node_names_of = Graph.keys o nodes_of;
    1.53  
    1.54 -fun get_node version name = Graph.get_node (nodes_of version) name
    1.55 -  handle Graph.UNDEF _ => empty_node;
    1.56 -
    1.57 -fun update_node name f =
    1.58 -  Graph.default_node (name, empty_node) #> Graph.map_node name f;
    1.59 +fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
    1.60  
    1.61  fun edit_nodes (name, node_edit) (Version nodes) =
    1.62    Version
    1.63      (case node_edit of
    1.64 -      Remove => perhaps (try (Graph.del_node name)) nodes
    1.65 +      Clear => update_node name clear_node nodes
    1.66      | Edits edits => update_node name (edit_node edits) nodes
    1.67 -    (* FIXME maintain deps; cycles!? *)
    1.68 -    | Header header => update_node name (set_header header) nodes);
    1.69 +    | Header header =>
    1.70 +        let
    1.71 +          val node = get_node nodes name;
    1.72 +          val nodes' = Graph.new_node (name, node) (remove_node name nodes);
    1.73 +          val parents =
    1.74 +            (case header of Exn.Res (_, parents, _) => parents | _ => [])
    1.75 +            |> filter (can (Graph.get_node nodes'));
    1.76 +          val (header', nodes'') =
    1.77 +            (header, Graph.add_deps_acyclic (name, parents) nodes')
    1.78 +              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes');
    1.79 +        in Graph.map_node name (set_header header') nodes'' end);
    1.80  
    1.81  fun put_node name node (Version nodes) =
    1.82    Version (nodes
    1.83 @@ -214,11 +226,11 @@
    1.84  
    1.85  fun get_theory state version_id pos name =
    1.86    let
    1.87 -    val last = get_last (get_node (the_version state version_id) name);
    1.88 +    val last = get_last (node_of (the_version state version_id) name);
    1.89      val st =
    1.90        (case Lazy.peek (the_exec state last) of
    1.91          SOME result => #2 (Exn.release result)
    1.92 -      | NONE => error ("Unfinished execution for theory " ^ quote name));
    1.93 +      | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos));
    1.94    in Toplevel.end_theory pos st end;
    1.95  
    1.96  
    1.97 @@ -263,41 +275,38 @@
    1.98  
    1.99  in
   1.100  
   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 _ =>
   1.105 -          Exn.capture (fn () =>
   1.106 -            let val master_dir = Path.dir (Path.explode node_name);  (* FIXME move to Scala side *)
   1.107 -            in Toplevel.modify_master (SOME master_dir) raw_tr end) ()
   1.108 -      | NONE => Exn.Res raw_tr) of
   1.109 -    Exn.Res tr =>
   1.110 -      let
   1.111 -        val is_init = is_some (Toplevel.init_of tr);
   1.112 -        val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   1.113 -        val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
   1.114 +fun run_command (node_name, node_header) raw_tr st =
   1.115 +  let
   1.116 +    val is_init = Toplevel.is_init raw_tr;
   1.117 +    val tr =
   1.118 +      if is_init then
   1.119 +        raw_tr |> Toplevel.modify_init (fn _ =>
   1.120 +          let
   1.121 +            (* FIXME get theories from document state *)
   1.122 +            (* FIXME provide files via Scala layer *)
   1.123 +            val (name, imports, uses) = Exn.release node_header;
   1.124 +            val master = SOME (Path.dir (Path.explode node_name));
   1.125 +          in Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses) end)
   1.126 +      else raw_tr;
   1.127  
   1.128 -        val start = Timing.start ();
   1.129 -        val (errs, result) =
   1.130 -          if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
   1.131 -          else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   1.132 -        val _ = timing tr (Timing.result start);
   1.133 -        val _ = List.app (Toplevel.error_msg tr) errs;
   1.134 -        val res =
   1.135 -          (case result of
   1.136 -            NONE => (Toplevel.status tr Markup.failed; (false, st))
   1.137 -          | SOME st' =>
   1.138 -             (Toplevel.status tr Markup.finished;
   1.139 -              proof_status tr st';
   1.140 -              if do_print then async_state tr st' else ();
   1.141 -              (true, st')));
   1.142 -      in res end
   1.143 -  | Exn.Exn exn =>
   1.144 -      if Exn.is_interrupt exn then reraise exn
   1.145 -      else
   1.146 -       (Toplevel.error_msg raw_tr (ML_Compiler.exn_message exn);
   1.147 -        Toplevel.status raw_tr Markup.failed;
   1.148 -        (false, Toplevel.toplevel)));
   1.149 +    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   1.150 +    val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
   1.151 +
   1.152 +    val start = Timing.start ();
   1.153 +    val (errs, result) =
   1.154 +      if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
   1.155 +      else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   1.156 +    val _ = timing tr (Timing.result start);
   1.157 +    val _ = List.app (Toplevel.error_msg tr) errs;
   1.158 +  in
   1.159 +    (case result of
   1.160 +      NONE => (Toplevel.status tr Markup.failed; (false, st))
   1.161 +    | SOME st' =>
   1.162 +       (Toplevel.status tr Markup.finished;
   1.163 +        proof_status tr st';
   1.164 +        if do_print then async_state tr st' else ();
   1.165 +        (true, st')))
   1.166 +  end;
   1.167  
   1.168  end;
   1.169  
   1.170 @@ -315,7 +324,7 @@
   1.171      NONE => true
   1.172    | SOME exec' => exec' <> exec);
   1.173  
   1.174 -fun new_exec name (id: command_id) (exec_id, updates, state) =
   1.175 +fun new_exec node_info (id: command_id) (exec_id, updates, state) =
   1.176    let
   1.177      val exec = the_exec state exec_id;
   1.178      val exec_id' = new_id ();
   1.179 @@ -325,7 +334,7 @@
   1.180          let
   1.181            val st = #2 (Lazy.force exec);
   1.182            val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
   1.183 -        in run_command name exec_tr st end);
   1.184 +        in run_command node_info exec_tr st end);
   1.185      val state' = define_exec exec_id' exec' state;
   1.186    in (exec_id', (id, exec_id') :: updates, state') end;
   1.187  
   1.188 @@ -338,8 +347,11 @@
   1.189      val new_version = fold edit_nodes edits old_version;
   1.190  
   1.191      fun update_node name (rev_updates, version, st) =
   1.192 -      let val node = get_node version name in
   1.193 -        (case first_entry NONE (is_changed (get_node old_version name)) node of
   1.194 +      let
   1.195 +        val node = node_of version name;
   1.196 +        val header = get_header node;
   1.197 +      in
   1.198 +        (case first_entry NONE (is_changed (node_of old_version name)) node of
   1.199            NONE => (rev_updates, version, st)
   1.200          | SOME ((prev, id), _) =>
   1.201              let
   1.202 @@ -348,12 +360,12 @@
   1.203                    NONE => no_id
   1.204                  | SOME prev_id => the_default no_id (the_entry node prev_id));
   1.205                val (last, rev_upds, st') =
   1.206 -                fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
   1.207 +                fold_entries (SOME id) (new_exec (name, header) o #2 o #1) node (prev_exec, [], st);
   1.208                val node' = node |> fold update_entry rev_upds |> set_last last;
   1.209              in (rev_upds @ rev_updates, put_node name node' version, st') end)
   1.210        end;
   1.211  
   1.212 -    (* FIXME proper node deps *)
   1.213 +    (* FIXME Graph.schedule *)
   1.214      val (rev_updates, new_version', state') =
   1.215        fold update_node (node_names_of new_version) ([], new_version, state);
   1.216      val state'' = define_version new_id new_version' state';
   1.217 @@ -380,7 +392,7 @@
   1.218            [fn () =>
   1.219              node_names_of version |> List.app (fn name =>
   1.220                fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
   1.221 -                  (get_node version name) ())];
   1.222 +                  (node_of version name) ())];
   1.223  
   1.224      in (versions, commands, execs, execution') end);
   1.225