more precise iterate_entries_after if start refers to last entry;
authorwenzelm
Fri Sep 02 15:21:40 2011 +0200 (2011-09-02 ago)
changeset 446455938beb84adc
parent 44644 317e4962dd0f
child 44652 1cc7df9ff83b
more precise iterate_entries_after if start refers to last entry;
do not assign exec states after bad theory init;
reject illegal theory header after end of theory;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Sep 02 11:52:13 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Sep 02 15:21:40 2011 +0200
     1.3 @@ -113,7 +113,12 @@
     1.4    map_node (fn (touched, header, perspective, entries, last_exec, result) =>
     1.5      (touched, header, perspective, f entries, last_exec, result));
     1.6  fun get_entries (Node {entries, ...}) = entries;
     1.7 -fun iterate_entries start f = Entries.iterate start f o get_entries;
     1.8 +
     1.9 +fun iterate_entries f = Entries.iterate NONE f o get_entries;
    1.10 +fun iterate_entries_after start f (Node {entries, ...}) =
    1.11 +  (case Entries.get_after entries start of
    1.12 +    NONE => I
    1.13 +  | SOME id => Entries.iterate (SOME id) f entries);
    1.14  
    1.15  fun get_last_exec (Node {last_exec, ...}) = last_exec;
    1.16  fun set_last_exec last_exec =
    1.17 @@ -347,9 +352,7 @@
    1.18      val _ = Multithreading.interrupted ();
    1.19      val _ = Toplevel.status tr Markup.forked;
    1.20      val start = Timing.start ();
    1.21 -    val (errs, result) =
    1.22 -      if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
    1.23 -      else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    1.24 +    val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    1.25      val _ = timing tr (Timing.result start);
    1.26      val _ = Toplevel.status tr Markup.joined;
    1.27      val _ = List.app (Toplevel.error_msg tr) errs;
    1.28 @@ -386,31 +389,51 @@
    1.29  
    1.30  local
    1.31  
    1.32 -fun last_common last_visible node0 node =
    1.33 +fun last_common state last_visible node0 node =
    1.34    let
    1.35 -    fun get_common ((prev, id), exec) (found, (_, visible)) =
    1.36 +    fun update_flags prev (visible, initial) =
    1.37 +      let
    1.38 +        val visible' = visible andalso prev <> last_visible;
    1.39 +        val initial' = initial andalso
    1.40 +          (case prev of
    1.41 +            NONE => true
    1.42 +          | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
    1.43 +      in (visible', initial') end;
    1.44 +    fun get_common ((prev, id), exec) (found, (_, flags)) =
    1.45        if found then NONE
    1.46        else
    1.47          let val found' = is_none exec orelse exec <> lookup_entry node0 id
    1.48 -        in SOME (found', (prev, visible andalso prev <> last_visible)) end;
    1.49 -    val (found, (common, visible)) = iterate_entries NONE get_common node (false, (NONE, true));
    1.50 -    val common' = if found then common else Entries.get_after (get_entries node) common;
    1.51 -    val visible' = visible andalso common' <> last_visible;
    1.52 -  in (common', visible') end;
    1.53 +        in SOME (found', (prev, update_flags prev flags)) end;
    1.54 +    val (found, (common, flags)) =
    1.55 +      iterate_entries get_common node (false, (NONE, (true, true)));
    1.56 +  in
    1.57 +    if found then (common, flags)
    1.58 +    else
    1.59 +      let val last = Entries.get_after (get_entries node) common
    1.60 +      in (last, update_flags last flags) end
    1.61 +  end;
    1.62 +
    1.63 +fun illegal_init () = error "Illegal theory header after end of theory";
    1.64  
    1.65 -fun new_exec state init command_id' (execs, exec) =
    1.66 -  let
    1.67 -    val (_, tr0) = the_command state command_id';
    1.68 -    val exec_id' = new_id ();
    1.69 -    val exec' =
    1.70 -      snd exec |> Lazy.map (fn (st, _) =>
    1.71 -        let val tr =
    1.72 -          Future.join tr0
    1.73 -          |> Toplevel.modify_init init
    1.74 -          |> Toplevel.put_id (print_id exec_id');
    1.75 -        in run_command tr st end)
    1.76 -      |> pair command_id';
    1.77 -  in ((exec_id', exec') :: execs, exec') end;
    1.78 +fun new_exec state bad_init command_id' (execs, exec, init) =
    1.79 +  if bad_init andalso is_none init then NONE
    1.80 +  else
    1.81 +    let
    1.82 +      val (name, tr0) = the_command state command_id';
    1.83 +      val (modify_init, init') =
    1.84 +        if Keyword.is_theory_begin name then
    1.85 +          (Toplevel.modify_init (the_default illegal_init init), NONE)
    1.86 +        else (I, init);
    1.87 +        val exec_id' = new_id ();
    1.88 +      val exec' =
    1.89 +        snd exec |> Lazy.map (fn (st, _) =>
    1.90 +          let val tr =
    1.91 +            Future.join tr0
    1.92 +            |> modify_init
    1.93 +            |> Toplevel.put_id (print_id exec_id');
    1.94 +          in run_command tr st end)
    1.95 +        |> pair command_id';
    1.96 +    in SOME ((exec_id', exec') :: execs, exec', init') end;
    1.97  
    1.98  fun make_required nodes =
    1.99    let
   1.100 @@ -422,6 +445,10 @@
   1.101          all_visible Symtab.empty;
   1.102    in Symtab.defined required end;
   1.103  
   1.104 +fun check_theory nodes name =
   1.105 +  is_some (Thy_Info.lookup_theory name) orelse  (* FIXME more robust!? *)
   1.106 +  is_some (Exn.get_res (get_header (get_node nodes name)));
   1.107 +
   1.108  fun init_theory deps name node =
   1.109    let
   1.110      val (thy_name, imports, uses) = Exn.release (get_header node);
   1.111 @@ -459,6 +486,8 @@
   1.112              let
   1.113                val node0 = node_of old_version name;
   1.114                fun init () = init_theory deps name node;
   1.115 +              val bad_init =
   1.116 +                not (check_theory nodes name andalso forall (check_theory nodes o #1) deps);
   1.117              in
   1.118                (singleton o Future.forks)
   1.119                  {name = "Document.update", group = NONE,
   1.120 @@ -467,18 +496,19 @@
   1.121                    let
   1.122                      val required = is_required name;
   1.123                      val last_visible = #2 (get_perspective node);
   1.124 -                    val (common, visible) = last_common last_visible node0 node;
   1.125 +                    val (common, (visible, initial)) = last_common state last_visible node0 node;
   1.126                      val common_exec = the_exec state (the_default_entry node common);
   1.127  
   1.128 -                    val (execs, exec) = ([], common_exec) |>
   1.129 +                    val (execs, exec, _) =
   1.130 +                      ([], common_exec, if initial then SOME init else NONE) |>
   1.131                        (visible orelse required) ?
   1.132 -                        iterate_entries (after_entry node common)
   1.133 +                        iterate_entries_after common
   1.134                            (fn ((prev, id), _) => fn res =>
   1.135                              if not required andalso prev = last_visible then NONE
   1.136 -                            else SOME (new_exec state init id res)) node;
   1.137 +                            else new_exec state bad_init id res) node;
   1.138  
   1.139                      val no_execs =
   1.140 -                      iterate_entries (after_entry node0 common)
   1.141 +                      iterate_entries_after common
   1.142                          (fn ((_, id0), exec0) => fn res =>
   1.143                            if is_none exec0 then NONE
   1.144                            else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
   1.145 @@ -538,7 +568,7 @@
   1.146              (singleton o Future.forks)
   1.147                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
   1.148                  deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
   1.149 -              (iterate_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
   1.150 +              (iterate_entries (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
   1.151  
   1.152      in (versions, commands, execs, execution) end);
   1.153