vacuous execution after first malformed command;
authorwenzelm
Sat Aug 11 19:34:36 2012 +0200 (2012-08-11 ago)
changeset 48772e46cd0d26481
parent 48771 2ea997196d04
child 48773 0e1bab274672
vacuous execution after first malformed command;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Aug 11 18:05:41 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Aug 11 19:34:36 2012 +0200
     1.3 @@ -53,6 +53,7 @@
     1.4    val imperative: (unit -> unit) -> transition -> transition
     1.5    val ignored: Position.T -> transition
     1.6    val malformed: Position.T -> string -> transition
     1.7 +  val is_malformed: transition -> bool
     1.8    val theory: (theory -> theory) -> transition -> transition
     1.9    val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
    1.10    val theory': (bool -> theory -> theory) -> transition -> transition
    1.11 @@ -412,8 +413,11 @@
    1.12  fun imperative f = keep (fn _ => f ());
    1.13  
    1.14  fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
    1.15 +
    1.16 +val malformed_name = "<malformed>";
    1.17  fun malformed pos msg =
    1.18 -  empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
    1.19 +  empty |> name malformed_name |> position pos |> imperative (fn () => error msg);
    1.20 +fun is_malformed tr = name_of tr = malformed_name;
    1.21  
    1.22  val unknown_theory = imperative (fn () => warning "Unknown theory context");
    1.23  val unknown_proof = imperative (fn () => warning "Unknown proof context");
     2.1 --- a/src/Pure/PIDE/command.ML	Sat Aug 11 18:05:41 2012 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Sat Aug 11 19:34:36 2012 +0200
     2.3 @@ -13,7 +13,8 @@
     2.4    val memo_value: 'a -> 'a memo
     2.5    val memo_eval: 'a memo -> 'a
     2.6    val memo_result: 'a memo -> 'a
     2.7 -  val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
     2.8 +  val run_command: Toplevel.transition ->
     2.9 +    Toplevel.state * bool -> (Toplevel.state * bool) * unit lazy
    2.10  end;
    2.11  
    2.12  structure Command: COMMAND =
    2.13 @@ -88,34 +89,37 @@
    2.14  
    2.15  in
    2.16  
    2.17 -fun run_command tr st =
    2.18 -  let
    2.19 -    val is_init = Toplevel.is_init tr;
    2.20 -    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    2.21 +fun run_command tr (st, malformed) =
    2.22 +  if malformed then ((Toplevel.toplevel, malformed), no_print)
    2.23 +  else
    2.24 +    let
    2.25 +      val malformed' = Toplevel.is_malformed tr;
    2.26 +      val is_init = Toplevel.is_init tr;
    2.27 +      val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    2.28  
    2.29 -    val _ = Multithreading.interrupted ();
    2.30 -    val _ = Toplevel.status tr Isabelle_Markup.forked;
    2.31 -    val start = Timing.start ();
    2.32 -    val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    2.33 -    val _ = timing tr (Timing.result start);
    2.34 -    val _ = Toplevel.status tr Isabelle_Markup.joined;
    2.35 -    val _ = List.app (Toplevel.error_msg tr) errs;
    2.36 -  in
    2.37 -    (case result of
    2.38 -      NONE =>
    2.39 -        let
    2.40 -          val _ = if null errs then Exn.interrupt () else ();
    2.41 -          val _ = Toplevel.status tr Isabelle_Markup.failed;
    2.42 -        in (st, no_print) end
    2.43 -    | SOME st' =>
    2.44 -        let
    2.45 -          val _ = Toplevel.status tr Isabelle_Markup.finished;
    2.46 -          val _ = proof_status tr st';
    2.47 -          val do_print =
    2.48 -            not is_init andalso
    2.49 -              (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    2.50 -        in (st', if do_print then print_state tr st' else no_print) end)
    2.51 -  end;
    2.52 +      val _ = Multithreading.interrupted ();
    2.53 +      val _ = Toplevel.status tr Isabelle_Markup.forked;
    2.54 +      val start = Timing.start ();
    2.55 +      val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    2.56 +      val _ = timing tr (Timing.result start);
    2.57 +      val _ = Toplevel.status tr Isabelle_Markup.joined;
    2.58 +      val _ = List.app (Toplevel.error_msg tr) errs;
    2.59 +    in
    2.60 +      (case result of
    2.61 +        NONE =>
    2.62 +          let
    2.63 +            val _ = if null errs then Exn.interrupt () else ();
    2.64 +            val _ = Toplevel.status tr Isabelle_Markup.failed;
    2.65 +          in ((st, malformed'), no_print) end
    2.66 +      | SOME st' =>
    2.67 +          let
    2.68 +            val _ = Toplevel.status tr Isabelle_Markup.finished;
    2.69 +            val _ = proof_status tr st';
    2.70 +            val do_print =
    2.71 +              not is_init andalso
    2.72 +                (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    2.73 +          in ((st', malformed'), if do_print then print_state tr st' else no_print) end)
    2.74 +    end;
    2.75  
    2.76  end;
    2.77  
     3.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 11 18:05:41 2012 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 11 19:34:36 2012 +0200
     3.3 @@ -63,8 +63,8 @@
     3.4  type perspective = (command_id -> bool) * command_id option;
     3.5  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
     3.6  
     3.7 -type exec = (Toplevel.state * unit lazy) Command.memo;  (*eval/print process*)
     3.8 -val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
     3.9 +type exec = ((Toplevel.state * bool) * unit lazy) Command.memo;  (*eval/print process*)
    3.10 +val no_exec = Command.memo_value ((Toplevel.toplevel, false), Lazy.value ());
    3.11  
    3.12  abstype node = Node of
    3.13   {header: node_header,  (*master directory, theory header, errors*)
    3.14 @@ -303,7 +303,7 @@
    3.15    let
    3.16      fun finished_theory node =
    3.17        (case Exn.capture (Command.memo_result o the) (get_result node) of
    3.18 -        Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
    3.19 +        Exn.Res ((st, _), _) => can (Toplevel.end_theory Position.none) st
    3.20        | _ => false);
    3.21  
    3.22      fun run node command_id exec =
    3.23 @@ -348,14 +348,14 @@
    3.24  
    3.25  fun stable_finished_theory node =
    3.26    is_some (Exn.get_res (Exn.capture (fn () =>
    3.27 -    fst (Command.memo_result (the (get_result node)))
    3.28 +    fst (fst (Command.memo_result (the (get_result node))))
    3.29      |> Toplevel.end_theory Position.none
    3.30      |> Global_Theory.join_proofs) ()));
    3.31  
    3.32  fun stable_command exec =
    3.33    (case Exn.capture Command.memo_result exec of
    3.34      Exn.Exn exn => not (Exn.is_interrupt exn)
    3.35 -  | Exn.Res (st, _) =>
    3.36 +  | Exn.Res ((st, _), _) =>
    3.37        (case try Toplevel.theory_of st of
    3.38          NONE => true
    3.39        | SOME thy => is_some (Exn.get_res (Exn.capture Global_Theory.join_recent_proofs thy))));
    3.40 @@ -387,10 +387,10 @@
    3.41            SOME thy => thy
    3.42          | NONE =>
    3.43              Toplevel.end_theory (Position.file_only import)
    3.44 -              (fst
    3.45 +              (fst (fst
    3.46                  (Command.memo_result
    3.47                    (the_default no_exec
    3.48 -                    (get_result (snd (the (AList.lookup (op =) imports import)))))))));
    3.49 +                    (get_result (snd (the (AList.lookup (op =) imports import))))))))));
    3.50    in Thy_Load.begin_theory master_dir header parents end;
    3.51  
    3.52  fun check_theory full name node =