--- a/src/Pure/Isar/toplevel.ML Sat Aug 11 18:05:41 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML Sat Aug 11 19:34:36 2012 +0200
@@ -53,6 +53,7 @@
val imperative: (unit -> unit) -> transition -> transition
val ignored: Position.T -> transition
val malformed: Position.T -> string -> transition
+ val is_malformed: transition -> bool
val theory: (theory -> theory) -> transition -> transition
val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
val theory': (bool -> theory -> theory) -> transition -> transition
@@ -412,8 +413,11 @@
fun imperative f = keep (fn _ => f ());
fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
+
+val malformed_name = "<malformed>";
fun malformed pos msg =
- empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
+ empty |> name malformed_name |> position pos |> imperative (fn () => error msg);
+fun is_malformed tr = name_of tr = malformed_name;
val unknown_theory = imperative (fn () => warning "Unknown theory context");
val unknown_proof = imperative (fn () => warning "Unknown proof context");
--- a/src/Pure/PIDE/command.ML Sat Aug 11 18:05:41 2012 +0200
+++ b/src/Pure/PIDE/command.ML Sat Aug 11 19:34:36 2012 +0200
@@ -13,7 +13,8 @@
val memo_value: 'a -> 'a memo
val memo_eval: 'a memo -> 'a
val memo_result: 'a memo -> 'a
- val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
+ val run_command: Toplevel.transition ->
+ Toplevel.state * bool -> (Toplevel.state * bool) * unit lazy
end;
structure Command: COMMAND =
@@ -88,34 +89,37 @@
in
-fun run_command tr st =
- let
- val is_init = Toplevel.is_init tr;
- val is_proof = Keyword.is_proof (Toplevel.name_of tr);
+fun run_command tr (st, malformed) =
+ if malformed then ((Toplevel.toplevel, malformed), no_print)
+ else
+ let
+ val malformed' = Toplevel.is_malformed tr;
+ val is_init = Toplevel.is_init tr;
+ val is_proof = Keyword.is_proof (Toplevel.name_of tr);
- val _ = Multithreading.interrupted ();
- val _ = Toplevel.status tr Isabelle_Markup.forked;
- val start = Timing.start ();
- val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
- val _ = timing tr (Timing.result start);
- val _ = Toplevel.status tr Isabelle_Markup.joined;
- val _ = List.app (Toplevel.error_msg tr) errs;
- in
- (case result of
- NONE =>
- let
- val _ = if null errs then Exn.interrupt () else ();
- val _ = Toplevel.status tr Isabelle_Markup.failed;
- in (st, no_print) end
- | SOME st' =>
- let
- val _ = Toplevel.status tr Isabelle_Markup.finished;
- val _ = proof_status tr st';
- val do_print =
- not is_init andalso
- (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
- in (st', if do_print then print_state tr st' else no_print) end)
- end;
+ val _ = Multithreading.interrupted ();
+ val _ = Toplevel.status tr Isabelle_Markup.forked;
+ val start = Timing.start ();
+ val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+ val _ = timing tr (Timing.result start);
+ val _ = Toplevel.status tr Isabelle_Markup.joined;
+ val _ = List.app (Toplevel.error_msg tr) errs;
+ in
+ (case result of
+ NONE =>
+ let
+ val _ = if null errs then Exn.interrupt () else ();
+ val _ = Toplevel.status tr Isabelle_Markup.failed;
+ in ((st, malformed'), no_print) end
+ | SOME st' =>
+ let
+ val _ = Toplevel.status tr Isabelle_Markup.finished;
+ val _ = proof_status tr st';
+ val do_print =
+ not is_init andalso
+ (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
+ in ((st', malformed'), if do_print then print_state tr st' else no_print) end)
+ end;
end;
--- a/src/Pure/PIDE/document.ML Sat Aug 11 18:05:41 2012 +0200
+++ b/src/Pure/PIDE/document.ML Sat Aug 11 19:34:36 2012 +0200
@@ -63,8 +63,8 @@
type perspective = (command_id -> bool) * command_id option;
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
-type exec = (Toplevel.state * unit lazy) Command.memo; (*eval/print process*)
-val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
+type exec = ((Toplevel.state * bool) * unit lazy) Command.memo; (*eval/print process*)
+val no_exec = Command.memo_value ((Toplevel.toplevel, false), Lazy.value ());
abstype node = Node of
{header: node_header, (*master directory, theory header, errors*)
@@ -303,7 +303,7 @@
let
fun finished_theory node =
(case Exn.capture (Command.memo_result o the) (get_result node) of
- Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
+ Exn.Res ((st, _), _) => can (Toplevel.end_theory Position.none) st
| _ => false);
fun run node command_id exec =
@@ -348,14 +348,14 @@
fun stable_finished_theory node =
is_some (Exn.get_res (Exn.capture (fn () =>
- fst (Command.memo_result (the (get_result node)))
+ fst (fst (Command.memo_result (the (get_result node))))
|> Toplevel.end_theory Position.none
|> Global_Theory.join_proofs) ()));
fun stable_command exec =
(case Exn.capture Command.memo_result exec of
Exn.Exn exn => not (Exn.is_interrupt exn)
- | Exn.Res (st, _) =>
+ | Exn.Res ((st, _), _) =>
(case try Toplevel.theory_of st of
NONE => true
| SOME thy => is_some (Exn.get_res (Exn.capture Global_Theory.join_recent_proofs thy))));
@@ -387,10 +387,10 @@
SOME thy => thy
| NONE =>
Toplevel.end_theory (Position.file_only import)
- (fst
+ (fst (fst
(Command.memo_result
(the_default no_exec
- (get_result (snd (the (AList.lookup (op =) imports import)))))))));
+ (get_result (snd (the (AList.lookup (op =) imports import))))))))));
in Thy_Load.begin_theory master_dir header parents end;
fun check_theory full name node =