# HG changeset patch
# User wenzelm
# Date 1350411780 -7200
# Node ID 619acbd7266443758fa22713d83665109a00c320
# Parent  eeaf1ec7eac29dcf3790d875928041dfc37f72b4
more proof method text position information;

diff -r eeaf1ec7eac2 -r 619acbd72664 src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Oct 16 20:23:00 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 eeaf1ec7eac2 -r 619acbd72664 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/HOL/Statespace/state_space.ML	Tue Oct 16 20:23:00 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 eeaf1ec7eac2 -r 619acbd72664 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/HOL/Tools/try0.ML	Tue Oct 16 20:23:00 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 eeaf1ec7eac2 -r 619acbd72664 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 16 20:23:00 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 eeaf1ec7eac2 -r 619acbd72664 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/Pure/Isar/method.ML	Tue Oct 16 20:23:00 2012 +0200
@@ -73,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 =
@@ -411,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 eeaf1ec7eac2 -r 619acbd72664 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 16 20:23:00 2012 +0200
@@ -77,30 +77,30 @@
   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 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 -> state -> state Seq.result Seq.seq
-  val apply_end_results: Method.text -> state -> state Seq.result 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
@@ -116,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 =
@@ -532,8 +534,8 @@
     SOME {goal, ...} => Isabelle_Markup.proof_state (Thm.nprems_of goal)
   | NONE => Markup.empty);
 
-fun method_error kind state =
-  Seq.single (Proof_Display.method_error kind (raw_goal state));
+fun method_error kind pos state =
+  Seq.single (Proof_Display.method_error kind pos (raw_goal state));
 
 
 
@@ -811,10 +813,11 @@
   #> 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 proof_results arg =
+  Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
+    method_error "initial" (Method.position arg));
 
-fun end_proof bot txt =
+fun end_proof bot (arg, immed) =
   Seq.APPEND (fn state =>
     state
     |> assert_forward
@@ -823,8 +826,8 @@
     |> assert_current_goal true
     |> using_facts []
     |> `before_qed |-> (refine o the_default Method.succeed_text)
-    |> Seq.maps (refine (Method.finish_text txt))
-    |> Seq.make_results, method_error "terminal")
+    |> 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 =
@@ -844,10 +847,14 @@
   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 = Seq.APPEND (apply text #> Seq.make_results, method_error "");
-fun apply_end_results text = Seq.APPEND (apply_end text #> Seq.make_results, method_error "");
+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);
 
 
 
@@ -952,12 +959,12 @@
     |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
   end;
 
-fun local_qeds txt =
-  end_proof false txt
+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 #> Seq.the_result finished_goal_error;
+fun local_qed arg = local_qeds arg #> Seq.the_result finished_goal_error;
 
 
 (* global goals *)
@@ -973,12 +980,12 @@
 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
+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 #> Seq.the_result finished_goal_error;
+fun global_qed arg = global_qeds arg #> Seq.the_result finished_goal_error;
 
 
 (* concluding steps *)
@@ -988,16 +995,16 @@
   #> 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);
+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 eeaf1ec7eac2 -r 619acbd72664 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Oct 16 20:23:00 2012 +0200
@@ -19,7 +19,8 @@
   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 -> {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
+  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
@@ -111,9 +112,11 @@
 
 (* method_error *)
 
-fun method_error kind {context = ctxt, facts, goal} = Seq.Error (fn () =>
+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:\n";
+    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
diff -r eeaf1ec7eac2 -r 619acbd72664 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/Pure/Isar/token.ML	Tue Oct 16 20:23:00 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 eeaf1ec7eac2 -r 619acbd72664 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Oct 16 20:23:00 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 *)