# HG changeset patch # User wenzelm # Date 1344706476 -7200 # Node ID e46cd0d2648181bd11134b06b8abef7993aa297d # Parent 2ea997196d048858035dcdb151634a8c57a1bc7c vacuous execution after first malformed command; diff -r 2ea997196d04 -r e46cd0d26481 src/Pure/Isar/toplevel.ML --- 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 "" |> position pos |> imperative I; + +val malformed_name = ""; fun malformed pos msg = - empty |> name "" |> 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"); diff -r 2ea997196d04 -r e46cd0d26481 src/Pure/PIDE/command.ML --- 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; diff -r 2ea997196d04 -r e46cd0d26481 src/Pure/PIDE/document.ML --- 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 =