# HG changeset patch
# User wenzelm
# Date 1422547669 -3600
# Node ID 513300fa2d09e18e2d91a3600cc39a83f0acc5e9
# Parent  ca459352d8c5365973baefa317417c8f9cf6b2d4
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.;

diff -r ca459352d8c5 -r 513300fa2d09 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Jan 29 16:35:29 2015 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Jan 29 17:07:49 2015 +0100
@@ -44,7 +44,6 @@
   val ignored: Position.T -> transition
   val is_ignored: transition -> bool
   val malformed: Position.T -> string -> transition
-  val is_malformed: transition -> bool
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
@@ -353,10 +352,8 @@
 fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
 fun is_ignored tr = name_of tr = "<ignored>";
 
-val malformed_name = "<malformed>";
 fun malformed pos msg =
-  empty |> name malformed_name |> position pos |> imperative (fn () => error msg);
-fun is_malformed tr = name_of tr = malformed_name;
+  empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
 
 val unknown_theory = imperative (fn () => warning "Unknown theory context");
 val unknown_proof = imperative (fn () => warning "Unknown proof context");
diff -r ca459352d8c5 -r 513300fa2d09 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Jan 29 16:35:29 2015 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Jan 29 17:07:49 2015 +0100
@@ -136,10 +136,8 @@
 
 (* eval *)
 
-type eval_state =
-  {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
-val init_eval_state =
-  {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
+type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state};
+val init_eval_state = {failed = false, command = Toplevel.empty, state = Toplevel.toplevel};
 
 datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
 
@@ -195,35 +193,31 @@
     SOME prf => status tr (Proof.status_markup prf)
   | NONE => ());
 
-fun eval_state keywords span tr ({malformed, state, ...}: eval_state) =
-  if malformed then
-    {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
-  else
-    let
-      val _ = Multithreading.interrupted ();
+fun eval_state keywords span tr ({state, ...}: eval_state) =
+  let
+    val _ = Multithreading.interrupted ();
 
-      val malformed' = Toplevel.is_malformed tr;
-      val st = reset_state keywords tr state;
+    val st = reset_state keywords tr state;
 
-      val _ = status tr Markup.running;
-      val (errs1, result) = run keywords true tr st;
-      val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
-      val errs = errs1 @ errs2;
-      val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
-    in
-      (case result of
-        NONE =>
-          let
-            val _ = status tr Markup.failed;
-            val _ = status tr Markup.finished;
-            val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
-          in {failed = true, malformed = malformed', command = tr, state = st} end
-      | SOME st' =>
-          let
-            val _ = proof_status tr st';
-            val _ = status tr Markup.finished;
-          in {failed = false, malformed = malformed', command = tr, state = st'} end)
-    end;
+    val _ = status tr Markup.running;
+    val (errs1, result) = run keywords true tr st;
+    val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
+    val errs = errs1 @ errs2;
+    val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
+  in
+    (case result of
+      NONE =>
+        let
+          val _ = status tr Markup.failed;
+          val _ = status tr Markup.finished;
+          val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
+        in {failed = true, command = tr, state = st} end
+    | SOME st' =>
+        let
+          val _ = proof_status tr st';
+          val _ = status tr Markup.finished;
+        in {failed = false, command = tr, state = st'} end)
+  end;
 
 in