1.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Oct 16 17:47:23 2012 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Oct 16 20:23:00 2012 +0200
     1.3 @@ -318,7 +318,7 @@
     1.4      Args.$$$ "narrow" |-- timeout "step_timeout" quick_timeout --
     1.5        timeout "final_timeout" default_timeout >> boogie_narrow_vc) --
     1.6    vc_name -- Method.parse >>
     1.7 -  (fn ((f, vc_name), meth) => f vc_name meth)
     1.8 +  (fn ((f, vc_name), (meth, _)) => f vc_name meth)
     1.9  
    1.10  val status_vc =
    1.11    (scan_arg

     2.1 --- a/src/HOL/Statespace/state_space.ML	Tue Oct 16 17:47:23 2012 +0200
     2.2 +++ b/src/HOL/Statespace/state_space.ML	Tue Oct 16 20:23:00 2012 +0200
     2.3 @@ -146,7 +146,7 @@
     2.4     thy
     2.5     |> Expression.sublocale_cmd I (name, Position.none) (expression_no_pos expr) []
     2.6     |> Proof.global_terminal_proof
     2.7 -         (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
     2.8 +         ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.none), NONE)
     2.9     |> Proof_Context.theory_of
    2.10  
    2.11  fun add_locale name expr elems thy =

     3.1 --- a/src/HOL/Tools/try0.ML	Tue Oct 16 17:47:23 2012 +0200
     3.2 +++ b/src/HOL/Tools/try0.ML	Tue Oct 16 20:23:00 2012 +0200
     3.3 @@ -55,7 +55,7 @@
     3.4    #> Outer_Syntax.scan Position.start
     3.5    #> filter Token.is_proper
     3.6    #> Scan.read Token.stopper Method.parse
     3.7 -  #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
     3.8 +  #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
     3.9  
    3.10  fun apply_named_method_on_first_goal method thy =
    3.11    method |> parse_method

     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Oct 16 17:47:23 2012 +0200
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 16 20:23:00 2012 +0200
     4.3 @@ -30,8 +30,8 @@
     4.4    val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
     4.5    val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
     4.6    val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
     4.7 -  val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
     4.8 -  val terminal_proof: Method.text * Method.text option ->
     4.9 +  val qed: Method.text_position option -> Toplevel.transition -> Toplevel.transition
    4.10 +  val terminal_proof: Method.text_position * Method.text_position option ->
    4.11      Toplevel.transition -> Toplevel.transition
    4.12    val default_proof: Toplevel.transition -> Toplevel.transition
    4.13    val immediate_proof: Toplevel.transition -> Toplevel.transition

     5.1 --- a/src/Pure/Isar/method.ML	Tue Oct 16 17:47:23 2012 +0200
     5.2 +++ b/src/Pure/Isar/method.ML	Tue Oct 16 20:23:00 2012 +0200
     5.3 @@ -73,7 +73,10 @@
     5.4    type modifier = (Proof.context -> Proof.context) * attribute
     5.5    val section: modifier parser list -> thm list context_parser
     5.6    val sections: modifier parser list -> thm list list context_parser
     5.7 -  val parse: text parser
     5.8 +  type text_position = text * Position.T
     5.9 +  val parse: text_position parser
    5.10 +  val text: text_position option -> text option
    5.11 +  val position: text_position option -> Position.T
    5.12  end;
    5.13  
    5.14  structure Method: METHOD =
    5.15 @@ -411,7 +414,23 @@
    5.16  and meth1 x = (Parse.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
    5.17  and meth0 x = (Parse.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
    5.18  
    5.19 -in val parse = meth3 end;
    5.20 +in
    5.21 +
    5.22 +val parse =
    5.23 +  Scan.trace meth3 >> (fn (m, toks) => (m, Position.set_range (Token.position_range_of toks)));
    5.24 +
    5.25 +end;
    5.26 +
    5.27 +
    5.28 +(* text position *)
    5.29 +
    5.30 +type text_position = text * Position.T;
    5.31 +
    5.32 +fun text NONE = NONE
    5.33 +  | text (SOME (txt, _)) = SOME txt;
    5.34 +
    5.35 +fun position NONE = Position.none
    5.36 +  | position (SOME (_, pos)) = pos;
    5.37  
    5.38  
    5.39  (* theory setup *)

     6.1 --- a/src/Pure/Isar/proof.ML	Tue Oct 16 17:47:23 2012 +0200
     6.2 +++ b/src/Pure/Isar/proof.ML	Tue Oct 16 20:23:00 2012 +0200
     6.3 @@ -77,30 +77,30 @@
     6.4    val begin_notepad: context -> state
     6.5    val end_notepad: state -> context
     6.6    val proof: Method.text option -> state -> state Seq.seq
     6.7 -  val proof_results: Method.text option -> state -> state Seq.result Seq.seq
     6.8 +  val proof_results: Method.text_position option -> state -> state Seq.result Seq.seq
     6.9    val defer: int -> state -> state
    6.10    val prefer: int -> state -> state
    6.11    val apply: Method.text -> state -> state Seq.seq
    6.12    val apply_end: Method.text -> state -> state Seq.seq
    6.13 -  val apply_results: Method.text -> state -> state Seq.result Seq.seq
    6.14 -  val apply_end_results: Method.text -> state -> state Seq.result Seq.seq
    6.15 +  val apply_results: Method.text_position -> state -> state Seq.result Seq.seq
    6.16 +  val apply_end_results: Method.text_position -> state -> state Seq.result Seq.seq
    6.17    val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
    6.18      (context -> 'a -> attribute) ->
    6.19      ('b list -> context -> (term list list * (context -> context)) * context) ->
    6.20      string -> Method.text option -> (thm list list -> state -> state) ->
    6.21      ((binding * 'a list) * 'b) list -> state -> state
    6.22 -  val local_qed: Method.text option * bool -> state -> state
    6.23 +  val local_qed: Method.text_position option * bool -> state -> state
    6.24    val theorem: Method.text option -> (thm list list -> context -> context) ->
    6.25      (term * term list) list list -> context -> state
    6.26    val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
    6.27      (string * string list) list list -> context -> state
    6.28 -  val global_qed: Method.text option * bool -> state -> context
    6.29 -  val local_terminal_proof: Method.text * Method.text option -> state -> state
    6.30 +  val global_qed: Method.text_position option * bool -> state -> context
    6.31 +  val local_terminal_proof: Method.text_position * Method.text_position option -> state -> state
    6.32    val local_default_proof: state -> state
    6.33    val local_immediate_proof: state -> state
    6.34    val local_skip_proof: bool -> state -> state
    6.35    val local_done_proof: state -> state
    6.36 -  val global_terminal_proof: Method.text * Method.text option -> state -> context
    6.37 +  val global_terminal_proof: Method.text_position * Method.text_position option -> state -> context
    6.38    val global_default_proof: state -> context
    6.39    val global_immediate_proof: state -> context
    6.40    val global_skip_proof: bool -> state -> context
    6.41 @@ -116,8 +116,10 @@
    6.42    val schematic_goal: state -> bool
    6.43    val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
    6.44    val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
    6.45 -  val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state
    6.46 -  val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
    6.47 +  val local_future_terminal_proof: Method.text_position * Method.text_position option -> bool ->
    6.48 +    state -> state
    6.49 +  val global_future_terminal_proof: Method.text_position * Method.text_position option -> bool ->
    6.50 +    state -> context
    6.51  end;
    6.52  
    6.53  structure Proof: PROOF =
    6.54 @@ -532,8 +534,8 @@
    6.55      SOME {goal, ...} => Isabelle_Markup.proof_state (Thm.nprems_of goal)
    6.56    | NONE => Markup.empty);
    6.57  
    6.58 -fun method_error kind state =
    6.59 -  Seq.single (Proof_Display.method_error kind (raw_goal state));
    6.60 +fun method_error kind pos state =
    6.61 +  Seq.single (Proof_Display.method_error kind pos (raw_goal state));
    6.62  
    6.63  
    6.64  
    6.65 @@ -811,10 +813,11 @@
    6.66    #> refine (the_default Method.default_text opt_text)
    6.67    #> Seq.map (using_facts [] #> enter_forward);
    6.68  
    6.69 -fun proof_results opt_text =
    6.70 -  Seq.APPEND (proof opt_text #> Seq.make_results, method_error "initial");
    6.71 +fun proof_results arg =
    6.72 +  Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
    6.73 +    method_error "initial" (Method.position arg));
    6.74  
    6.75 -fun end_proof bot txt =
    6.76 +fun end_proof bot (arg, immed) =
    6.77    Seq.APPEND (fn state =>
    6.78      state
    6.79      |> assert_forward
    6.80 @@ -823,8 +826,8 @@
    6.81      |> assert_current_goal true
    6.82      |> using_facts []
    6.83      |> `before_qed |-> (refine o the_default Method.succeed_text)
    6.84 -    |> Seq.maps (refine (Method.finish_text txt))
    6.85 -    |> Seq.make_results, method_error "terminal")
    6.86 +    |> Seq.maps (refine (Method.finish_text (Method.text arg, immed)))
    6.87 +    |> Seq.make_results, method_error "terminal" (Method.position arg))
    6.88    #> Seq.maps_results (Seq.single o finished_goal);
    6.89  
    6.90  fun check_result msg sq =
    6.91 @@ -844,10 +847,14 @@
    6.92    refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))) #> Seq.hd;
    6.93  
    6.94  fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
    6.95 +
    6.96  fun apply_end text = assert_forward #> refine_end text;
    6.97  
    6.98 -fun apply_results text = Seq.APPEND (apply text #> Seq.make_results, method_error "");
    6.99 -fun apply_end_results text = Seq.APPEND (apply_end text #> Seq.make_results, method_error "");
   6.100 +fun apply_results (text, pos) =
   6.101 +  Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
   6.102 +
   6.103 +fun apply_end_results (text, pos) =
   6.104 +  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
   6.105  
   6.106  
   6.107  
   6.108 @@ -952,12 +959,12 @@
   6.109      |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
   6.110    end;
   6.111  
   6.112 -fun local_qeds txt =
   6.113 -  end_proof false txt
   6.114 +fun local_qeds arg =
   6.115 +  end_proof false arg
   6.116    #> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
   6.117      (fn ((after_qed, _), results) => after_qed results));
   6.118  
   6.119 -fun local_qed txt = local_qeds txt #> Seq.the_result finished_goal_error;
   6.120 +fun local_qed arg = local_qeds arg #> Seq.the_result finished_goal_error;
   6.121  
   6.122  
   6.123  (* global goals *)
   6.124 @@ -973,12 +980,12 @@
   6.125  val theorem = global_goal Proof_Context.bind_propp_schematic_i;
   6.126  val theorem_cmd = global_goal Proof_Context.bind_propp_schematic;
   6.127  
   6.128 -fun global_qeds txt =
   6.129 -  end_proof true txt
   6.130 +fun global_qeds arg =
   6.131 +  end_proof true arg
   6.132    #> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
   6.133      after_qed results (context_of state)));
   6.134  
   6.135 -fun global_qed txt = global_qeds txt #> Seq.the_result finished_goal_error;
   6.136 +fun global_qed arg = global_qeds arg #> Seq.the_result finished_goal_error;
   6.137  
   6.138  
   6.139  (* concluding steps *)
   6.140 @@ -988,16 +995,16 @@
   6.141    #> Seq.the_result "";
   6.142  
   6.143  fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
   6.144 -val local_default_proof = local_terminal_proof (Method.default_text, NONE);
   6.145 -val local_immediate_proof = local_terminal_proof (Method.this_text, NONE);
   6.146 -fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE);
   6.147 -val local_done_proof = terminal_proof local_qeds Method.done_text (NONE, false);
   6.148 +val local_default_proof = local_terminal_proof ((Method.default_text, Position.none), NONE);
   6.149 +val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.none), NONE);
   6.150 +fun local_skip_proof int = local_terminal_proof ((Method.sorry_text int, Position.none), NONE);
   6.151 +val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.none) (NONE, false);
   6.152  
   6.153  fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
   6.154 -val global_default_proof = global_terminal_proof (Method.default_text, NONE);
   6.155 -val global_immediate_proof = global_terminal_proof (Method.this_text, NONE);
   6.156 -fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE);
   6.157 -val global_done_proof = terminal_proof global_qeds Method.done_text (NONE, false);
   6.158 +val global_default_proof = global_terminal_proof ((Method.default_text, Position.none), NONE);
   6.159 +val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.none), NONE);
   6.160 +fun global_skip_proof int = global_terminal_proof ((Method.sorry_text int, Position.none), NONE);
   6.161 +val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.none) (NONE, false);
   6.162  
   6.163  
   6.164  (* common goal statements *)

     7.1 --- a/src/Pure/Isar/proof_display.ML	Tue Oct 16 17:47:23 2012 +0200
     7.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Oct 16 20:23:00 2012 +0200
     7.3 @@ -19,7 +19,8 @@
     7.4    val string_of_rule: Proof.context -> string -> thm -> string
     7.5    val pretty_goal_header: thm -> Pretty.T
     7.6    val string_of_goal: Proof.context -> thm -> string
     7.7 -  val method_error: string -> {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
     7.8 +  val method_error: string -> Position.T ->
     7.9 +    {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
    7.10    val print_results: Markup.T -> bool -> Proof.context ->
    7.11      ((string * string) * (string * thm list) list) -> unit
    7.12    val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
    7.13 @@ -111,9 +112,11 @@
    7.14  
    7.15  (* method_error *)
    7.16  
    7.17 -fun method_error kind {context = ctxt, facts, goal} = Seq.Error (fn () =>
    7.18 +fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
    7.19    let
    7.20 -    val pr_header = "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^ "proof method:\n";
    7.21 +    val pr_header =
    7.22 +      "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
    7.23 +      "proof method" ^ Position.here pos ^ ":\n";
    7.24      val pr_facts =
    7.25        if null facts then ""
    7.26        else

     8.1 --- a/src/Pure/Isar/token.ML	Tue Oct 16 17:47:23 2012 +0200
     8.2 +++ b/src/Pure/Isar/token.ML	Tue Oct 16 20:23:00 2012 +0200
     8.3 @@ -18,6 +18,7 @@
     8.4    val str_of_kind: kind -> string
     8.5    val position_of: T -> Position.T
     8.6    val end_position_of: T -> Position.T
     8.7 +  val position_range_of: T list -> Position.range
     8.8    val pos_of: T -> string
     8.9    val eof: T
    8.10    val is_eof: T -> bool
    8.11 @@ -130,6 +131,9 @@
    8.12  fun position_of (Token ((_, (pos, _)), _, _)) = pos;
    8.13  fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
    8.14  
    8.15 +fun position_range_of [] = Position.no_range
    8.16 +  | position_range_of toks = (position_of (hd toks), end_position_of (List.last toks));
    8.17 +
    8.18  val pos_of = Position.here o position_of;
    8.19  
    8.20  

     9.1 --- a/src/Pure/PIDE/command.ML	Tue Oct 16 17:47:23 2012 +0200
     9.2 +++ b/src/Pure/PIDE/command.ML	Tue Oct 16 20:23:00 2012 +0200
     9.3 @@ -22,14 +22,8 @@
     9.4  
     9.5  (* span range *)
     9.6  
     9.7 -fun range [] = (Position.none, Position.none)
     9.8 -  | range toks =
     9.9 -      let
    9.10 -        val start_pos = Token.position_of (hd toks);
    9.11 -        val end_pos = Token.end_position_of (List.last toks);
    9.12 -      in (start_pos, end_pos) end;
    9.13 -
    9.14 -val proper_range = range o #1 o take_suffix Token.is_space;
    9.15 +val range = Token.position_range_of;
    9.16 +val proper_range = Token.position_range_of o #1 o take_suffix Token.is_space;
    9.17  
    9.18  
    9.19  (* memo results *)