# HG changeset patch
# User wenzelm
# Date 1350393252 -7200
# Node ID b5fb6e7f8d819cd5ce2b43ec66cbad026e92cabc
# Parent  fb2d8ba7d3a9f54b2e4f2e0d2e24ff2b34988259
more informative errors for 'proof' and 'apply' steps;
more Seq.result operations;

diff -r fb2d8ba7d3a9 -r b5fb6e7f8d81 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/General/seq.ML	Tue Oct 16 15:14:12 2012 +0200
@@ -36,9 +36,12 @@
   val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
   val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
   datatype 'a result = Result of 'a | Error of unit -> string
+  val make_results: 'a seq -> 'a result seq
+  val filter_results: 'a result seq -> 'a seq
   val maps_results: ('a -> 'b result seq) -> 'a result seq -> 'b result seq
   val maps_result: ('a -> 'b seq) -> 'a result seq -> 'b result seq
   val map_result: ('a -> 'b) -> 'a result seq -> 'b result seq
+  val first_result: string -> 'a result seq -> 'a * 'a seq
   val the_result: string -> 'a result seq -> 'a
   val succeed: 'a -> 'a seq
   val fail: 'a -> 'b seq
@@ -205,6 +208,9 @@
 
 datatype 'a result = Result of 'a | Error of unit -> string;
 
+fun make_results xq = map Result xq;
+fun filter_results xq = map_filter (fn Result x => SOME x | Error _ => NONE) xq;
+
 fun maps_results f xq =
   make (fn () =>
     (case pull xq of
@@ -216,17 +222,19 @@
 fun map_result f = maps_result (single o f);
 
 (*first result or first error within sequence*)
-fun the_result default_msg seq =
+fun first_result default_msg seq =
   let
     fun result opt_msg xq =
       (case (opt_msg, pull xq) of
-        (_, SOME (Result x, _)) => x
+        (_, SOME (Result x, xq')) => (x, filter_results xq')
       | (SOME _, SOME (Error _, xq')) => result opt_msg xq'
       | (NONE, SOME (Error msg, xq')) => result (SOME msg) xq'
       | (SOME msg, NONE) => error (msg ())
       | (NONE, NONE) => error (if default_msg = "" then "Empty result sequence" else default_msg));
   in result NONE seq end;
 
+fun the_result default_msg seq = #1 (first_result default_msg seq);
+
 
 
 (** sequence functions **)      (*cf. Pure/tactical.ML*)
diff -r fb2d8ba7d3a9 -r b5fb6e7f8d81 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 16 15:14:12 2012 +0200
@@ -681,24 +681,25 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
-    (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
+    (Scan.option Parse.nat >> (fn n =>
+      (Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.defer n))));
 
 val _ =
   Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
-    (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
+    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.prefer n)));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
-    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
+    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement (unstructured)"
-    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
+    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
 
 val _ =
   Outer_Syntax.command @{command_spec "proof"} "backward proof"
     (Scan.option Method.parse >> (fn m => Toplevel.print o
-      Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
+      Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
       Toplevel.skip_proof (fn i => i + 1)));
 
 
@@ -709,12 +710,12 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
-    (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
+    (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.also_cmd args)));
 
 val _ =
   Outer_Syntax.command @{command_spec "finally"}
     "combine calculation and current facts, exhibit result"
-    (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
+    (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.finally_cmd args)));
 
 val _ =
   Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
diff -r fb2d8ba7d3a9 -r b5fb6e7f8d81 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 16 15:14:12 2012 +0200
@@ -77,10 +77,13 @@
   val begin_notepad: context -> state
   val end_notepad: state -> context
   val proof: Method.text option -> state -> state Seq.seq
+  val proof_results: Method.text option -> state -> state Seq.result Seq.seq
   val defer: int option -> state -> state Seq.seq
   val prefer: int -> state -> state Seq.seq
   val apply: Method.text -> state -> state Seq.seq
   val apply_end: Method.text -> state -> state Seq.seq
+  val apply_results: Method.text -> state -> state Seq.result Seq.seq
+  val apply_end_results: Method.text -> state -> state Seq.result Seq.seq
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (context -> 'a -> attribute) ->
     ('b list -> context -> (term list list * (context -> context)) * context) ->
@@ -529,8 +532,8 @@
     SOME {goal, ...} => Isabelle_Markup.proof_state (Thm.nprems_of goal)
   | NONE => Markup.empty);
 
-fun method_error name state =
-  Seq.single (Proof_Display.method_error name (raw_goal state));
+fun method_error kind state =
+  Seq.single (Proof_Display.method_error kind (raw_goal state));
 
 
 
@@ -808,6 +811,9 @@
   #> refine (the_default Method.default_text opt_text)
   #> Seq.map (using_facts [] #> enter_forward);
 
+fun proof_results opt_text =
+  Seq.APPEND (proof opt_text #> Seq.make_results, method_error "initial");
+
 fun end_proof bot txt =
   Seq.APPEND (fn state =>
     state
@@ -818,7 +824,7 @@
     |> using_facts []
     |> `before_qed |-> (refine o the_default Method.succeed_text)
     |> Seq.maps (refine (Method.finish_text txt))
-    |> Seq.map Seq.Result, method_error "terminal")
+    |> Seq.make_results, method_error "terminal")
   #> Seq.maps_results (Seq.single o finished_goal);
 
 fun check_result msg sq =
@@ -835,6 +841,9 @@
 fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
 fun apply_end text = assert_forward #> refine_end text;
 
+fun apply_results text = Seq.APPEND (apply text #> Seq.make_results, method_error "");
+fun apply_end_results text = Seq.APPEND (apply_end text #> Seq.make_results, method_error "");
+
 
 
 (** goals **)
@@ -970,8 +979,8 @@
 (* concluding steps *)
 
 fun terminal_proof qeds initial terminal =
-  Seq.APPEND (proof (SOME initial) #> Seq.map Seq.Result, method_error "initial")
-  #> Seq.maps_results (qeds terminal) #> Seq.the_result "";
+  proof_results (SOME initial) #> Seq.maps_results (qeds terminal)
+  #> Seq.the_result "";
 
 fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
 val local_default_proof = local_terminal_proof (Method.default_text, NONE);
diff -r fb2d8ba7d3a9 -r b5fb6e7f8d81 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Oct 16 15:14:12 2012 +0200
@@ -111,9 +111,9 @@
 
 (* method_error *)
 
-fun method_error name {context = ctxt, facts, goal} = Seq.Error (fn () =>
+fun method_error kind {context = ctxt, facts, goal} = Seq.Error (fn () =>
   let
-    val pr_header = "Failure of " ^ (if name = "" then "" else name ^ " ") ^ "proof method:\n";
+    val pr_header = "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^ "proof method:\n";
     val pr_facts =
       if null facts then ""
       else
diff -r fb2d8ba7d3a9 -r b5fb6e7f8d81 src/Pure/Isar/proof_node.ML
--- a/src/Pure/Isar/proof_node.ML	Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/Isar/proof_node.ML	Tue Oct 16 15:14:12 2012 +0200
@@ -11,7 +11,7 @@
   val current: T -> Proof.state
   val position: T -> int
   val back: T -> T
-  val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
+  val applys: (Proof.state -> Proof.state Seq.result Seq.seq) -> T -> T
   val apply: (Proof.state -> Proof.state) -> T -> T
 end;
 
@@ -42,10 +42,8 @@
 (* apply transformer *)
 
 fun applys f (Proof_Node ((st, _), n)) =
-  (case Seq.pull (f st) of
-    NONE => error "empty result sequence -- proof command failed"
-  | SOME res => Proof_Node (res, n + 1));
+  Proof_Node (Seq.first_result "Empty result sequence -- proof command failed" (f st), n + 1);
 
-fun apply f = applys (Seq.single o f);
+fun apply f = applys (Seq.single o Seq.Result o f);
 
 end;
diff -r fb2d8ba7d3a9 -r b5fb6e7f8d81 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Oct 16 15:14:12 2012 +0200
@@ -74,9 +74,9 @@
   val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
   val forget_proof: transition -> transition
   val present_proof: (state -> unit) -> transition -> transition
-  val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
+  val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
-  val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
+  val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
   val proof: (Proof.state -> Proof.state) -> transition -> transition
   val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
   val skip_proof: (int -> int) -> transition -> transition
@@ -556,7 +556,7 @@
     | skip as SkipProof _ => skip
     | _ => raise UNDEF));
 
-fun proof' f = proofs' (Seq.single oo f);
+fun proof' f = proofs' ((Seq.single o Seq.Result) oo f);
 val proofs = proofs' o K;
 val proof = proof' o K;