discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
authorwenzelm
Thu Jan 29 17:07:49 2015 +0100 (2015-01-29 ago)
changeset 59472513300fa2d09
parent 59471 ca459352d8c5
child 59473 b0ac740fc510
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jan 29 16:35:29 2015 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jan 29 17:07:49 2015 +0100
     1.3 @@ -44,7 +44,6 @@
     1.4    val ignored: Position.T -> transition
     1.5    val is_ignored: transition -> bool
     1.6    val malformed: Position.T -> string -> transition
     1.7 -  val is_malformed: transition -> bool
     1.8    val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
     1.9    val theory': (bool -> theory -> theory) -> transition -> transition
    1.10    val theory: (theory -> theory) -> transition -> transition
    1.11 @@ -353,10 +352,8 @@
    1.12  fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
    1.13  fun is_ignored tr = name_of tr = "<ignored>";
    1.14  
    1.15 -val malformed_name = "<malformed>";
    1.16  fun malformed pos msg =
    1.17 -  empty |> name malformed_name |> position pos |> imperative (fn () => error msg);
    1.18 -fun is_malformed tr = name_of tr = malformed_name;
    1.19 +  empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
    1.20  
    1.21  val unknown_theory = imperative (fn () => warning "Unknown theory context");
    1.22  val unknown_proof = imperative (fn () => warning "Unknown proof context");
     2.1 --- a/src/Pure/PIDE/command.ML	Thu Jan 29 16:35:29 2015 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Thu Jan 29 17:07:49 2015 +0100
     2.3 @@ -136,10 +136,8 @@
     2.4  
     2.5  (* eval *)
     2.6  
     2.7 -type eval_state =
     2.8 -  {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
     2.9 -val init_eval_state =
    2.10 -  {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    2.11 +type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state};
    2.12 +val init_eval_state = {failed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    2.13  
    2.14  datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
    2.15  
    2.16 @@ -195,35 +193,31 @@
    2.17      SOME prf => status tr (Proof.status_markup prf)
    2.18    | NONE => ());
    2.19  
    2.20 -fun eval_state keywords span tr ({malformed, state, ...}: eval_state) =
    2.21 -  if malformed then
    2.22 -    {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
    2.23 -  else
    2.24 -    let
    2.25 -      val _ = Multithreading.interrupted ();
    2.26 +fun eval_state keywords span tr ({state, ...}: eval_state) =
    2.27 +  let
    2.28 +    val _ = Multithreading.interrupted ();
    2.29  
    2.30 -      val malformed' = Toplevel.is_malformed tr;
    2.31 -      val st = reset_state keywords tr state;
    2.32 +    val st = reset_state keywords tr state;
    2.33  
    2.34 -      val _ = status tr Markup.running;
    2.35 -      val (errs1, result) = run keywords true tr st;
    2.36 -      val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
    2.37 -      val errs = errs1 @ errs2;
    2.38 -      val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
    2.39 -    in
    2.40 -      (case result of
    2.41 -        NONE =>
    2.42 -          let
    2.43 -            val _ = status tr Markup.failed;
    2.44 -            val _ = status tr Markup.finished;
    2.45 -            val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
    2.46 -          in {failed = true, malformed = malformed', command = tr, state = st} end
    2.47 -      | SOME st' =>
    2.48 -          let
    2.49 -            val _ = proof_status tr st';
    2.50 -            val _ = status tr Markup.finished;
    2.51 -          in {failed = false, malformed = malformed', command = tr, state = st'} end)
    2.52 -    end;
    2.53 +    val _ = status tr Markup.running;
    2.54 +    val (errs1, result) = run keywords true tr st;
    2.55 +    val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
    2.56 +    val errs = errs1 @ errs2;
    2.57 +    val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
    2.58 +  in
    2.59 +    (case result of
    2.60 +      NONE =>
    2.61 +        let
    2.62 +          val _ = status tr Markup.failed;
    2.63 +          val _ = status tr Markup.finished;
    2.64 +          val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
    2.65 +        in {failed = true, command = tr, state = st} end
    2.66 +    | SOME st' =>
    2.67 +        let
    2.68 +          val _ = proof_status tr st';
    2.69 +          val _ = status tr Markup.finished;
    2.70 +        in {failed = false, command = tr, state = st'} end)
    2.71 +  end;
    2.72  
    2.73  in
    2.74