src/Pure/PIDE/document.ML
changeset 52534 341ae9cd4743
parent 52533 a95440dcd59c
child 52536 3a35ce87a55c
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 05 17:09:28 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 05 18:37:44 2013 +0200
     1.3 @@ -109,8 +109,8 @@
     1.4    map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
     1.5  
     1.6  fun finished_theory node =
     1.7 -  (case Exn.capture (Command.eval_result o the) (get_result node) of
     1.8 -    Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
     1.9 +  (case Exn.capture (Command.eval_result_state o the) (get_result node) of
    1.10 +    Exn.Res st => can (Toplevel.end_theory Position.none) st
    1.11    | _ => false);
    1.12  
    1.13  fun get_node nodes name = String_Graph.get_node nodes name
    1.14 @@ -347,10 +347,9 @@
    1.15            SOME thy => thy
    1.16          | NONE =>
    1.17              Toplevel.end_theory (Position.file_only import)
    1.18 -              (#state
    1.19 -                (Command.eval_result
    1.20 -                  (the_default Command.no_eval
    1.21 -                    (get_result (snd (the (AList.lookup (op =) deps import)))))))));
    1.22 +              (Command.eval_result_state
    1.23 +                (the_default Command.no_eval
    1.24 +                  (get_result (snd (the (AList.lookup (op =) deps import))))))));
    1.25      val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
    1.26    in Thy_Load.begin_theory master_dir header parents end;
    1.27  
    1.28 @@ -391,31 +390,16 @@
    1.29      else (common, flags)
    1.30    end;
    1.31  
    1.32 +fun illegal_init _ = error "Illegal theory header after end of theory";
    1.33 +
    1.34  fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
    1.35    if not proper_init andalso is_none init then NONE
    1.36    else
    1.37      let
    1.38 +      val (_, (eval, _)) = command_exec;
    1.39        val (command_name, span) = the_command state command_id' ||> Lazy.force;
    1.40 -
    1.41 -      fun illegal_init _ = error "Illegal theory header after end of theory";
    1.42 -      val (modify_init, init') =
    1.43 -        if Keyword.is_theory_begin command_name then
    1.44 -          (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
    1.45 -        else (I, init);
    1.46 -
    1.47 -      val exec_id' = Document_ID.make ();
    1.48 -      val eval_body' =
    1.49 -        Command.memo (fn () =>
    1.50 -          let
    1.51 -            val eval_state = Command.exec_result (snd command_exec);
    1.52 -            val tr =
    1.53 -              Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id'))
    1.54 -                (fn () =>
    1.55 -                  Command.read span
    1.56 -                  |> modify_init
    1.57 -                  |> Toplevel.put_id exec_id') ();
    1.58 -          in Command.eval span tr eval_state end);
    1.59 -      val eval' = {exec_id = exec_id', eval = eval_body'};
    1.60 +      val init' = if Keyword.is_theory_begin command_name then NONE else init;
    1.61 +      val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
    1.62        val prints' = if command_visible then Command.print command_name eval' else [];
    1.63        val command_exec' = (command_id', (eval', prints'));
    1.64      in SOME (command_exec' :: execs, command_exec', init') end;