# HG changeset patch
# User wenzelm
# Date 1350419914 -7200
# Node ID 9db36f881137b654282f6027d432bba591dec6ba
# Parent  a6ebdaf8e2679977cfee762923330849be3c09f4# Parent  2b82358694e62d1bff926befd37928e721ee6d95
merged

diff -r a6ebdaf8e267 -r 9db36f881137 NEWS
--- a/NEWS	Tue Oct 16 20:31:08 2012 +0200
+++ b/NEWS	Tue Oct 16 22:38:34 2012 +0200
@@ -41,6 +41,9 @@
 specifications: nesting of "context fixes ... context assumes ..."
 and "class ... context ...".
 
+* More informative error messages for Isar proof commands involving
+lazy enumerations (method applications etc.).
+
 
 *** Pure ***
 
@@ -201,6 +204,10 @@
 
 *** ML ***
 
+* Type Seq.results and related operations support embedded error
+messages within lazy enumerations, and thus allow to provide
+informative errors in the absence of any usable results.
+
 * Renamed Position.str_of to Position.here to emphasize that this is a
 formal device to inline positions into message text, but not
 necessarily printing visible text.
diff -r a6ebdaf8e267 -r 9db36f881137 src/Doc/IsarImplementation/Integration.thy
--- a/src/Doc/IsarImplementation/Integration.thy	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Doc/IsarImplementation/Integration.thy	Tue Oct 16 22:38:34 2012 +0200
@@ -154,7 +154,7 @@
   Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
   Toplevel.transition -> Toplevel.transition"} \\
-  @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) ->
+  @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) ->
   Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) ->
   Toplevel.transition -> Toplevel.transition"} \\
diff -r a6ebdaf8e267 -r 9db36f881137 src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -10,7 +10,6 @@
 sig
   val ss_only: thm list -> simpset
 
-  val prefer_tac: int -> tactic
   val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
   val fo_rtac: thm -> Proof.context -> int -> tactic
   val unfold_thms_tac: Proof.context -> thm list -> tactic
@@ -39,9 +38,6 @@
 
 fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms;
 
-(* FIXME: why not in "Pure"? *)
-fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1);
-
 fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
   tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
 
diff -r a6ebdaf8e267 -r 9db36f881137 src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -318,7 +318,7 @@
     Args.$$$ "narrow" |-- timeout "step_timeout" quick_timeout --
       timeout "final_timeout" default_timeout >> boogie_narrow_vc) --
   vc_name -- Method.parse >>
-  (fn ((f, vc_name), meth) => f vc_name meth)
+  (fn ((f, vc_name), (meth, _)) => f vc_name meth)
 
 val status_vc =
   (scan_arg
diff -r a6ebdaf8e267 -r 9db36f881137 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/HOL/Statespace/state_space.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -146,7 +146,7 @@
    thy
    |> Expression.sublocale_cmd I (name, Position.none) (expression_no_pos expr) []
    |> Proof.global_terminal_proof
-         (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
+         ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.none), NONE)
    |> Proof_Context.theory_of
 
 fun add_locale name expr elems thy =
diff -r a6ebdaf8e267 -r 9db36f881137 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/HOL/Tools/try0.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -55,7 +55,7 @@
   #> Outer_Syntax.scan Position.start
   #> filter Token.is_proper
   #> Scan.read Token.stopper Method.parse
-  #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
+  #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
 
 fun apply_named_method_on_first_goal method thy =
   method |> parse_method
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/General/seq.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -35,6 +35,14 @@
   val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq
   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
   val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
@@ -110,7 +118,7 @@
 fun of_list xs = fold_rev cons xs empty;
 
 
-(*sequence append:  put the elements of xq in front of those of yq*)
+(*sequence append: put the elements of xq in front of those of yq*)
 fun append xq yq =
   let
     fun copy s =
@@ -161,7 +169,12 @@
       NONE => NONE
     | SOME (x, xq') => SOME (f x, map f xq')));
 
-fun maps f = flat o map f;
+fun maps f xq =
+  make (fn () =>
+    (case pull xq of
+      NONE => NONE
+    | SOME (x, xq') => pull (append (f x) (maps f xq'))));
+
 fun map_filter f = maps (fn x => (case f x of NONE => empty | SOME y => single y));
 
 fun lift f xq y = map (fn x => f x y) xq;
@@ -191,6 +204,38 @@
   in its xq end;
 
 
+(* embedded errors *)
+
+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
+      NONE => NONE
+    | SOME (Result x, xq') => pull (append (f x) (maps_results f xq'))
+    | SOME (Error msg, xq') => SOME (Error msg, maps_results f xq')));
+
+fun maps_result f = maps_results (map Result o f);
+fun map_result f = maps_result (single o f);
+
+(*first result or first error within sequence*)
+fun first_result default_msg seq =
+  let
+    fun result opt_msg xq =
+      (case (opt_msg, pull xq) of
+        (_, 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 a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/Isar/calculation.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -13,12 +13,12 @@
   val sym_add: attribute
   val sym_del: attribute
   val symmetric: attribute
-  val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
+  val also: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
   val also_cmd: (Facts.ref * Attrib.src list) list option ->
-    bool -> Proof.state -> Proof.state Seq.seq
-  val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
+    bool -> Proof.state -> Proof.state Seq.result Seq.seq
+  val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
   val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
-    Proof.state -> Proof.state Seq.seq
+    Proof.state -> Proof.state Seq.result Seq.seq
   val moreover: bool -> Proof.state -> Proof.state
   val ultimately: bool -> Proof.state -> Proof.state
 end;
@@ -129,32 +129,48 @@
 fun calculate prep_rules final raw_rules int state =
   let
     val ctxt = Proof.context_of state;
+    val pretty_thm = Display.pretty_thm ctxt;
 
     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
     val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
-    fun projection ths th = exists (curry eq_prop th) ths;
+    fun check_projection ths th =
+      (case find_index (curry eq_prop th) ths of
+        ~1 => Seq.Result [th]
+      | i =>
+          Seq.Error (fn () =>
+            (Pretty.string_of o Pretty.chunks)
+             [Pretty.block [Pretty.str "Vacuous calculation result:", Pretty.brk 1, pretty_thm th],
+              (Pretty.block o Pretty.fbreaks)
+                (Pretty.str ("derived as projection (" ^ string_of_int (i + 1) ^ ") from:") ::
+                  map pretty_thm ths)]));
 
     val opt_rules = Option.map (prep_rules ctxt) raw_rules;
     fun combine ths =
-      (case opt_rules of SOME rules => rules
-      | NONE =>
-          (case ths of
-            [] => Item_Net.content (#1 (get_rules ctxt))
-          | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th)))
-      |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
-      |> Seq.filter (not o projection ths);
+      Seq.append
+        ((case opt_rules of
+          SOME rules => rules
+        | NONE =>
+            (case ths of
+              [] => Item_Net.content (#1 (get_rules ctxt))
+            | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th)))
+        |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
+        |> Seq.map (check_projection ths))
+        (Seq.single (Seq.Error (fn () =>
+          (Pretty.string_of o Pretty.block o Pretty.fbreaks)
+            (Pretty.str "No matching trans rules for calculation:" ::
+              map pretty_thm ths))));
 
     val facts = Proof.the_facts (assert_sane final state);
     val (initial, calculations) =
       (case get_calculation state of
-        NONE => (true, Seq.single facts)
-      | SOME calc => (false, Seq.map single (combine (calc @ facts))));
+        NONE => (true, Seq.single (Seq.Result facts))
+      | SOME calc => (false, combine (calc @ facts)));
 
     val _ = initial andalso final andalso error "No calculation yet";
     val _ = initial andalso is_some opt_rules andalso
       error "Initial calculation -- no rules to be given";
   in
-    calculations |> Seq.map (fn calc => maintain_calculation int final calc state)
+    calculations |> Seq.map_result (fn calc => maintain_calculation int final calc state)
   end;
 
 val also = calculate (K I) false;
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -30,8 +30,8 @@
   val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
-  val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
-  val terminal_proof: Method.text * Method.text option ->
+  val qed: Method.text_position option -> Toplevel.transition -> Toplevel.transition
+  val terminal_proof: Method.text_position * Method.text_position option ->
     Toplevel.transition -> Toplevel.transition
   val default_proof: Toplevel.transition -> Toplevel.transition
   val immediate_proof: Toplevel.transition -> Toplevel.transition
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -681,24 +681,24 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
-    (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
+    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (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.proof (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)));
 
 
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/Isar/method.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -20,8 +20,6 @@
   val SIMPLE_METHOD: tactic -> method
   val SIMPLE_METHOD': (int -> tactic) -> method
   val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
-  val defer: int option -> method
-  val prefer: int -> method
   val cheating: bool -> Proof.context -> method
   val intro: thm list -> method
   val elim: thm list -> method
@@ -75,7 +73,10 @@
   type modifier = (Proof.context -> Proof.context) * attribute
   val section: modifier parser list -> thm list context_parser
   val sections: modifier parser list -> thm list list context_parser
-  val parse: text parser
+  type text_position = text * Position.T
+  val parse: text_position parser
+  val text: text_position option -> text option
+  val position: text_position option -> Position.T
 end;
 
 structure Method: METHOD =
@@ -124,12 +125,6 @@
 end;
 
 
-(* shuffle subgoals *)
-
-fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)));
-fun defer opt_i = METHOD (K (Tactic.defer_tac (the_default 1 opt_i)));
-
-
 (* cheating *)
 
 fun cheating int ctxt =
@@ -419,7 +414,23 @@
 and meth1 x = (Parse.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
 and meth0 x = (Parse.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
 
-in val parse = meth3 end;
+in
+
+val parse =
+  Scan.trace meth3 >> (fn (m, toks) => (m, Position.set_range (Token.position_range_of toks)));
+
+end;
+
+
+(* text position *)
+
+type text_position = text * Position.T;
+
+fun text NONE = NONE
+  | text (SOME (txt, _)) = SOME txt;
+
+fun position NONE = Position.none
+  | position (SOME (_, pos)) = pos;
 
 
 (* theory setup *)
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -77,27 +77,30 @@
   val begin_notepad: context -> state
   val end_notepad: state -> context
   val proof: Method.text option -> state -> state Seq.seq
-  val defer: int option -> state -> state Seq.seq
-  val prefer: int -> state -> state Seq.seq
+  val proof_results: Method.text_position option -> state -> state Seq.result Seq.seq
+  val defer: int -> state -> state
+  val prefer: int -> state -> state
   val apply: Method.text -> state -> state Seq.seq
   val apply_end: Method.text -> state -> state Seq.seq
+  val apply_results: Method.text_position -> state -> state Seq.result Seq.seq
+  val apply_end_results: Method.text_position -> 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) ->
     string -> Method.text option -> (thm list list -> state -> state) ->
     ((binding * 'a list) * 'b) list -> state -> state
-  val local_qed: Method.text option * bool -> state -> state
+  val local_qed: Method.text_position option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
     (term * term list) list list -> context -> state
   val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
     (string * string list) list list -> context -> state
-  val global_qed: Method.text option * bool -> state -> context
-  val local_terminal_proof: Method.text * Method.text option -> state -> state
+  val global_qed: Method.text_position option * bool -> state -> context
+  val local_terminal_proof: Method.text_position * Method.text_position option -> state -> state
   val local_default_proof: state -> state
   val local_immediate_proof: state -> state
   val local_skip_proof: bool -> state -> state
   val local_done_proof: state -> state
-  val global_terminal_proof: Method.text * Method.text option -> state -> context
+  val global_terminal_proof: Method.text_position * Method.text_position option -> state -> context
   val global_default_proof: state -> context
   val global_immediate_proof: state -> context
   val global_skip_proof: bool -> state -> context
@@ -113,8 +116,10 @@
   val schematic_goal: state -> bool
   val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
   val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
-  val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state
-  val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
+  val local_future_terminal_proof: Method.text_position * Method.text_position option -> bool ->
+    state -> state
+  val global_future_terminal_proof: Method.text_position * Method.text_position option -> bool ->
+    state -> context
 end;
 
 structure Proof: PROOF =
@@ -333,32 +338,20 @@
 
 fun pretty_facts _ _ NONE = []
   | pretty_facts s ctxt (SOME ths) =
-      [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
+      [(Pretty.block o Pretty.fbreaks)
+        (Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"] ::
+          map (Display.pretty_thm ctxt) ths), Pretty.str ""];
 
 fun pretty_state nr state =
   let
     val {context = ctxt, facts, mode, goal = _} = top state;
     val verbose = Config.get ctxt Proof_Context.verbose;
 
-    fun levels_up 0 = ""
-      | levels_up 1 = "1 level up"
-      | levels_up i = string_of_int i ^ " levels up";
-
-    fun subgoals 0 = ""
-      | subgoals 1 = "1 subgoal"
-      | subgoals n = string_of_int n ^ " subgoals";
-
-    fun description strs =
-      (case filter_out (fn s => s = "") strs of [] => ""
-      | strs' => enclose " (" ")" (commas strs'));
-
-    fun prt_goal (SOME (_, (i,
+    fun prt_goal (SOME (_, (_,
       {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
           pretty_facts "using " ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
-          [Pretty.str ("goal" ^
-            description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
-          Goal_Display.pretty_goals ctxt goal @
+          [Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @
           (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
       | prt_goal NONE = [];
 
@@ -487,8 +480,7 @@
     val string_of_term = Syntax.string_of_term ctxt;
     val string_of_thm = Display.string_of_thm ctxt;
 
-    val _ = Thm.no_prems goal orelse
-      error (Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt goal));
+    val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
 
     val extra_hyps = Assumption.extra_hyps ctxt goal;
     val _ = null extra_hyps orelse
@@ -514,20 +506,13 @@
       | recover_result _ _ = lost_structure ();
   in recover_result propss results end;
 
-fun the_finished_goal results =
-  (case Seq.pull results of
-    SOME ((f1, state1), rest) =>
-      let val (ctxt1, (_, goal1)) = get_goal state1 in
-        if Thm.no_prems goal1 then f1 state1
-        else
-          (case Seq.pull (Seq.filter (Thm.no_prems o #2 o #2 o get_goal o #2) rest) of
-            SOME ((f, state), _) => f state
-          | NONE =>
-              error ("Failed to finish proof:\n" ^
-                Pretty.string_of
-                  (Goal_Display.pretty_goal {main = true, limit = false} ctxt1 goal1)))
-      end
-  | NONE => error "Failed to finish proof");
+val finished_goal_error = "Failed to finish proof";
+
+fun finished_goal state =
+  let val (ctxt, (_, goal)) = get_goal state in
+    if Thm.no_prems goal then Seq.Result state
+    else Seq.Error (fn () => finished_goal_error ^ ":\n" ^ Proof_Display.string_of_goal ctxt goal)
+  end;
 
 
 (* goal views -- corresponding to methods *)
@@ -549,6 +534,9 @@
     SOME {goal, ...} => Isabelle_Markup.proof_state (Thm.nprems_of goal)
   | NONE => Markup.empty);
 
+fun method_error kind pos state =
+  Seq.single (Proof_Display.method_error kind pos (raw_goal state));
+
 
 
 (*** structured proof commands ***)
@@ -825,15 +813,22 @@
   #> refine (the_default Method.default_text opt_text)
   #> Seq.map (using_facts [] #> enter_forward);
 
-fun end_proof bot txt state =
-  state
-  |> assert_forward
-  |> assert_bottom bot
-  |> close_block
-  |> assert_current_goal true
-  |> using_facts []
-  |> `before_qed |-> (refine o the_default Method.succeed_text)
-  |> Seq.maps (refine (Method.finish_text txt));
+fun proof_results arg =
+  Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
+    method_error "initial" (Method.position arg));
+
+fun end_proof bot (arg, immed) =
+  Seq.APPEND (fn state =>
+    state
+    |> assert_forward
+    |> assert_bottom bot
+    |> close_block
+    |> assert_current_goal true
+    |> using_facts []
+    |> `before_qed |-> (refine o the_default Method.succeed_text)
+    |> Seq.maps (refine (Method.finish_text (Method.text arg, immed)))
+    |> Seq.make_results, method_error "terminal" (Method.position arg))
+  #> Seq.maps_results (Seq.single o finished_goal);
 
 fun check_result msg sq =
   (case Seq.pull sq of
@@ -843,12 +838,24 @@
 
 (* unstructured refinement *)
 
-fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i)));
-fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i)));
+fun defer i =
+  assert_no_chain #>
+  refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))) #> Seq.hd;
+
+fun prefer i =
+  assert_no_chain #>
+  refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))) #> Seq.hd;
 
 fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
+
 fun apply_end text = assert_forward #> refine_end text;
 
+fun apply_results (text, pos) =
+  Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
+
+fun apply_end_results (text, pos) =
+  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
+
 
 
 (** goals **)
@@ -952,12 +959,12 @@
     |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
   end;
 
-fun local_qeds txt =
-  end_proof false txt
-  #> Seq.map (pair (generic_qed Proof_Context.auto_bind_facts #->
-    (fn ((after_qed, _), results) => after_qed results)));
+fun local_qeds arg =
+  end_proof false arg
+  #> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
+    (fn ((after_qed, _), results) => after_qed results));
 
-fun local_qed txt = local_qeds txt #> the_finished_goal;
+fun local_qed arg = local_qeds arg #> Seq.the_result finished_goal_error;
 
 
 (* global goals *)
@@ -973,51 +980,31 @@
 val theorem = global_goal Proof_Context.bind_propp_schematic_i;
 val theorem_cmd = global_goal Proof_Context.bind_propp_schematic;
 
-fun global_qeds txt =
-  end_proof true txt
-  #> Seq.map (pair (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
-    after_qed results (context_of state))));
+fun global_qeds arg =
+  end_proof true arg
+  #> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
+    after_qed results (context_of state)));
 
-fun global_qed txt = global_qeds txt #> the_finished_goal;
+fun global_qed arg = global_qeds arg #> Seq.the_result finished_goal_error;
 
 
 (* concluding steps *)
 
-local
-
-fun failure_initial state =
-  let
-    val (ctxt, (facts, goal)) = get_goal state;
-    val pr_facts =
-      if null facts then ""
-      else Pretty.string_of (Pretty.big_list "facts:" (map (Display.pretty_thm ctxt) facts)) ^ "\n";
-    val pr_goal =
-      "goal:\n" ^ Pretty.string_of (Goal_Display.pretty_goal {main = false, limit = false} ctxt goal);
-  in error ("Failure of initial proof method on goal state:\n" ^ pr_facts ^ pr_goal) end;
-
-fun failure_terminal _ = error "Failure of terminal proof method";
-
-val op ORELSE = Seq.ORELSE;
-
 fun terminal_proof qeds initial terminal =
-  (((proof (SOME initial) ORELSE failure_initial)
-    #> Seq.maps (qeds terminal)) ORELSE failure_terminal) #> the_finished_goal;
-
-in
+  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);
-val local_immediate_proof = local_terminal_proof (Method.this_text, NONE);
-fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE);
-val local_done_proof = terminal_proof local_qeds Method.done_text (NONE, false);
+val local_default_proof = local_terminal_proof ((Method.default_text, Position.none), NONE);
+val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.none), NONE);
+fun local_skip_proof int = local_terminal_proof ((Method.sorry_text int, Position.none), NONE);
+val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.none) (NONE, false);
 
 fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
-val global_default_proof = global_terminal_proof (Method.default_text, NONE);
-val global_immediate_proof = global_terminal_proof (Method.this_text, NONE);
-fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE);
-val global_done_proof = terminal_proof global_qeds Method.done_text (NONE, false);
-
-end;
+val global_default_proof = global_terminal_proof ((Method.default_text, Position.none), NONE);
+val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.none), NONE);
+fun global_skip_proof int = global_terminal_proof ((Method.sorry_text int, Position.none), NONE);
+val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.none) (NONE, false);
 
 
 (* common goal statements *)
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -17,6 +17,10 @@
   val pretty_full_theory: bool -> theory -> Pretty.T
   val print_theory: theory -> unit
   val string_of_rule: Proof.context -> string -> thm -> string
+  val pretty_goal_header: thm -> Pretty.T
+  val string_of_goal: Proof.context -> thm -> string
+  val method_error: string -> Position.T ->
+    {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
   val print_results: Markup.T -> bool -> Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
   val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
@@ -86,6 +90,43 @@
 val string_of_rule = Pretty.string_of ooo pretty_rule;
 
 
+(* goals *)
+
+local
+
+fun subgoals 0 = []
+  | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"]
+  | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")];
+
+in
+
+fun pretty_goal_header goal =
+  Pretty.block ([Pretty.command "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
+
+end;
+
+fun string_of_goal ctxt goal =
+  Pretty.string_of (Pretty.chunks
+    [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]);
+
+
+(* method_error *)
+
+fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
+  let
+    val pr_header =
+      "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
+      "proof method" ^ Position.here pos ^ ":\n";
+    val pr_facts =
+      if null facts then ""
+      else
+        (Pretty.string_of o Pretty.block o Pretty.fbreaks)
+          (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] ::
+            map (Display.pretty_thm ctxt) facts) ^ "\n";
+    val pr_goal = string_of_goal ctxt goal;
+  in pr_header ^ pr_facts ^ pr_goal end);
+
+
 (* results *)
 
 local
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/proof_node.ML
--- a/src/Pure/Isar/proof_node.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/Isar/proof_node.ML	Tue Oct 16 22:38:34 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 a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/Isar/token.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -18,6 +18,7 @@
   val str_of_kind: kind -> string
   val position_of: T -> Position.T
   val end_position_of: T -> Position.T
+  val position_range_of: T list -> Position.range
   val pos_of: T -> string
   val eof: T
   val is_eof: T -> bool
@@ -130,6 +131,9 @@
 fun position_of (Token ((_, (pos, _)), _, _)) = pos;
 fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
 
+fun position_range_of [] = Position.no_range
+  | position_range_of toks = (position_of (hd toks), end_position_of (List.last toks));
+
 val pos_of = Position.here o position_of;
 
 
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Oct 16 22:38:34 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;
 
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -22,14 +22,8 @@
 
 (* span range *)
 
-fun range [] = (Position.none, Position.none)
-  | range toks =
-      let
-        val start_pos = Token.position_of (hd toks);
-        val end_pos = Token.end_position_of (List.last toks);
-      in (start_pos, end_pos) end;
-
-val proper_range = range o #1 o take_suffix Token.is_space;
+val range = Token.position_range_of;
+val proper_range = Token.position_range_of o #1 o take_suffix Token.is_space;
 
 
 (* memo results *)
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/ROOT.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -305,17 +305,6 @@
 use "ProofGeneral/proof_general_emacs.ML";
 
 
-(* the Pure theory *)
-
-use "pure_syn.ML";
-Thy_Info.use_thy ("Pure", Position.none);
-Context.set_thread_data NONE;
-structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
-
-
-use "ProofGeneral/pgip_tests.ML";
-
-
 (* ML toplevel pretty printing *)
 
 toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
@@ -326,7 +315,6 @@
 toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
 toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
 toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
-toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
 toplevel_pp ["Context", "theory"] "Context.pretty_thy";
 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
@@ -339,6 +327,18 @@
 if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
 
 
+(* the Pure theory *)
+
+use "pure_syn.ML";
+Toplevel.program (fn () => Thy_Info.use_thy ("Pure", Position.none));
+Context.set_thread_data NONE;
+structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
+
+toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
+
+use "ProofGeneral/pgip_tests.ML";
+
+
 (* ML toplevel commands *)
 
 fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/logic.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -557,8 +557,10 @@
 
 (* goal states *)
 
-fun get_goal st i = nth_prem (i, st)
-  handle TERM _ => error "Goal number out of range";
+fun get_goal st i =
+  nth_prem (i, st) handle TERM _ =>
+    error ("Subgoal number " ^ string_of_int i ^ " out of range (a total of " ^
+      string_of_int (count_prems st)  ^ " subgoals)");
 
 (*reverses parameters for substitution*)
 fun goal_params st i =
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/tactic.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -53,6 +53,7 @@
   val rename_tac: string list -> int -> tactic
   val rotate_tac: int -> int -> tactic
   val defer_tac: int -> tactic
+  val prefer_tac: int -> tactic
   val filter_prems_tac: (term -> bool) -> int -> tactic
 end;
 
@@ -318,6 +319,9 @@
 (*Rotates the given subgoal to be the last.*)
 fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1);
 
+(*Rotates the given subgoal to be the first.*)
+fun prefer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1 #> Thm.permute_prems 0 ~1);
+
 (* remove premises that do not satisfy p; fails if all prems satisfy p *)
 fun filter_prems_tac p =
   let fun Then NONE tac = SOME tac
diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Pure/tactical.ML	Tue Oct 16 22:38:34 2012 +0200
@@ -55,6 +55,7 @@
   val TRYALL: (int -> tactic) -> tactic
   val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic
   val SUBGOAL: ((term * int) -> tactic) -> int -> tactic
+  val ASSERT_SUBGOAL: (int -> tactic) -> int -> tactic
   val CHANGED_GOAL: (int -> tactic) -> int -> tactic
   val SOLVED': (int -> tactic) -> int -> tactic
   val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic
@@ -328,6 +329,8 @@
 fun SUBGOAL goalfun =
   CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i));
 
+fun ASSERT_SUBGOAL (tac: int -> tactic) i st = (Logic.get_goal (Thm.prop_of st) i; tac i st);
+
 (*Returns all states that have changed in subgoal i, counted from the LAST
   subgoal.  For stac, for example.*)
 fun CHANGED_GOAL tac i st =
diff -r a6ebdaf8e267 -r 9db36f881137 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Tue Oct 16 20:31:08 2012 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Tue Oct 16 22:38:34 2012 +0200
@@ -16,7 +16,7 @@
 
 import java.lang.System
 import java.awt.BorderLayout
-import java.awt.event.{ComponentEvent, ComponentAdapter}
+import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}
 
 import org.gjt.sp.jedit.View
 
@@ -28,17 +28,20 @@
   private var implicit_snapshot = Document.State.init.snapshot()
   private var implicit_info: XML.Body = Nil
 
-  def apply(view: View, snapshot: Document.Snapshot, info: XML.Body)
+  private def set_implicit(snapshot: Document.Snapshot, info: XML.Body)
   {
     Swing_Thread.require()
 
     implicit_snapshot = snapshot
     implicit_info = info
+  }
 
-    view.getDockableWindowManager.floatDockableWindow("isabelle-info")
+  private def reset_implicit(): Unit = set_implicit(Document.State.init.snapshot(), Nil)
 
-    implicit_snapshot = Document.State.init.snapshot()
-    implicit_info = Nil
+  def apply(view: View, snapshot: Document.Snapshot, info: XML.Body)
+  {
+    set_implicit(snapshot, info)
+    view.getDockableWindowManager.floatDockableWindow("isabelle-info")
   }
 }
 
@@ -52,13 +55,22 @@
 
   private var zoom_factor = 100
 
+  private val snapshot = Info_Dockable.implicit_snapshot
+  private val info = Info_Dockable.implicit_info
+
+  private val window_focus_listener =
+    new WindowFocusListener {
+      def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, info) }
+      def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
+    }
+
 
   /* pretty text area */
 
   private val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
-  pretty_text_area.update(Info_Dockable.implicit_snapshot, Info_Dockable.implicit_info)
+  pretty_text_area.update(snapshot, info)
 
   private def handle_resize()
   {
@@ -85,6 +97,7 @@
   {
     Swing_Thread.require()
 
+    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
     Isabelle.session.global_options += main_actor
     handle_resize()
   }
@@ -93,6 +106,7 @@
   {
     Swing_Thread.require()
 
+    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
     Isabelle.session.global_options -= main_actor
     delay_resize.revoke()
   }