more method position information, notably finished_pos after end of previous text;
authorwenzelm
Wed Oct 17 13:20:08 2012 +0200 (2012-10-17 ago)
changeset 4988900ea087e83d8
parent 49888 ff2063be8227
child 49890 89eff795f757
more method position information, notably finished_pos after end of previous text;
src/HOL/Statespace/state_space.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
     1.1 --- a/src/HOL/Statespace/state_space.ML	Wed Oct 17 10:46:14 2012 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Oct 17 13:20:08 2012 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4     thy
     1.5     |> Expression.sublocale_cmd I (name, Position.none) (expression_no_pos expr) []
     1.6     |> Proof.global_terminal_proof
     1.7 -         ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.none), NONE)
     1.8 +         ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
     1.9     |> Proof_Context.theory_of
    1.10  
    1.11  fun add_locale name expr elems thy =
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Oct 17 10:46:14 2012 +0200
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 17 13:20:08 2012 +0200
     2.3 @@ -30,8 +30,8 @@
     2.4    val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
     2.5    val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
     2.6    val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
     2.7 -  val qed: Method.text_position option -> Toplevel.transition -> Toplevel.transition
     2.8 -  val terminal_proof: Method.text_position * Method.text_position option ->
     2.9 +  val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
    2.10 +  val terminal_proof: Method.text_range * Method.text_range option ->
    2.11      Toplevel.transition -> Toplevel.transition
    2.12    val default_proof: Toplevel.transition -> Toplevel.transition
    2.13    val immediate_proof: Toplevel.transition -> Toplevel.transition
     3.1 --- a/src/Pure/Isar/method.ML	Wed Oct 17 10:46:14 2012 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Wed Oct 17 13:20:08 2012 +0200
     3.3 @@ -73,10 +73,10 @@
     3.4    type modifier = (Proof.context -> Proof.context) * attribute
     3.5    val section: modifier parser list -> thm list context_parser
     3.6    val sections: modifier parser list -> thm list list context_parser
     3.7 -  type text_position = text * Position.T
     3.8 -  val parse: text_position parser
     3.9 -  val text: text_position option -> text option
    3.10 -  val position: text_position option -> Position.T
    3.11 +  type text_range = text * Position.range
    3.12 +  val parse: text_range parser
    3.13 +  val text: text_range option -> text option
    3.14 +  val position: text_range option -> Position.T
    3.15  end;
    3.16  
    3.17  structure Method: METHOD =
    3.18 @@ -417,20 +417,20 @@
    3.19  in
    3.20  
    3.21  val parse =
    3.22 -  Scan.trace meth3 >> (fn (m, toks) => (m, Position.set_range (Token.position_range_of toks)));
    3.23 +  Scan.trace meth3 >> (fn (m, toks) => (m, Token.position_range_of toks));
    3.24  
    3.25  end;
    3.26  
    3.27  
    3.28  (* text position *)
    3.29  
    3.30 -type text_position = text * Position.T;
    3.31 +type text_range = text * Position.range;
    3.32  
    3.33  fun text NONE = NONE
    3.34    | text (SOME (txt, _)) = SOME txt;
    3.35  
    3.36  fun position NONE = Position.none
    3.37 -  | position (SOME (_, pos)) = pos;
    3.38 +  | position (SOME (_, range)) = Position.set_range range;
    3.39  
    3.40  
    3.41  (* theory setup *)
     4.1 --- a/src/Pure/Isar/proof.ML	Wed Oct 17 10:46:14 2012 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Wed Oct 17 13:20:08 2012 +0200
     4.3 @@ -77,30 +77,30 @@
     4.4    val begin_notepad: context -> state
     4.5    val end_notepad: state -> context
     4.6    val proof: Method.text option -> state -> state Seq.seq
     4.7 -  val proof_results: Method.text_position option -> state -> state Seq.result Seq.seq
     4.8 +  val proof_results: Method.text_range option -> state -> state Seq.result Seq.seq
     4.9    val defer: int -> state -> state
    4.10    val prefer: int -> state -> state
    4.11    val apply: Method.text -> state -> state Seq.seq
    4.12    val apply_end: Method.text -> state -> state Seq.seq
    4.13 -  val apply_results: Method.text_position -> state -> state Seq.result Seq.seq
    4.14 -  val apply_end_results: Method.text_position -> state -> state Seq.result Seq.seq
    4.15 +  val apply_results: Method.text_range -> state -> state Seq.result Seq.seq
    4.16 +  val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
    4.17    val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
    4.18      (context -> 'a -> attribute) ->
    4.19      ('b list -> context -> (term list list * (context -> context)) * context) ->
    4.20      string -> Method.text option -> (thm list list -> state -> state) ->
    4.21      ((binding * 'a list) * 'b) list -> state -> state
    4.22 -  val local_qed: Method.text_position option * bool -> state -> state
    4.23 +  val local_qed: Method.text_range option * bool -> state -> state
    4.24    val theorem: Method.text option -> (thm list list -> context -> context) ->
    4.25      (term * term list) list list -> context -> state
    4.26    val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
    4.27      (string * string list) list list -> context -> state
    4.28 -  val global_qed: Method.text_position option * bool -> state -> context
    4.29 -  val local_terminal_proof: Method.text_position * Method.text_position option -> state -> state
    4.30 +  val global_qed: Method.text_range option * bool -> state -> context
    4.31 +  val local_terminal_proof: Method.text_range * Method.text_range option -> state -> state
    4.32    val local_default_proof: state -> state
    4.33    val local_immediate_proof: state -> state
    4.34    val local_skip_proof: bool -> state -> state
    4.35    val local_done_proof: state -> state
    4.36 -  val global_terminal_proof: Method.text_position * Method.text_position option -> state -> context
    4.37 +  val global_terminal_proof: Method.text_range * Method.text_range option -> state -> context
    4.38    val global_default_proof: state -> context
    4.39    val global_immediate_proof: state -> context
    4.40    val global_skip_proof: bool -> state -> context
    4.41 @@ -116,9 +116,9 @@
    4.42    val schematic_goal: state -> bool
    4.43    val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
    4.44    val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
    4.45 -  val local_future_terminal_proof: Method.text_position * Method.text_position option -> bool ->
    4.46 +  val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
    4.47      state -> state
    4.48 -  val global_future_terminal_proof: Method.text_position * Method.text_position option -> bool ->
    4.49 +  val global_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
    4.50      state -> context
    4.51  end;
    4.52  
    4.53 @@ -508,10 +508,13 @@
    4.54  
    4.55  val finished_goal_error = "Failed to finish proof";
    4.56  
    4.57 -fun finished_goal state =
    4.58 +fun finished_goal pos state =
    4.59    let val (ctxt, (_, goal)) = get_goal state in
    4.60      if Thm.no_prems goal then Seq.Result state
    4.61 -    else Seq.Error (fn () => finished_goal_error ^ ":\n" ^ Proof_Display.string_of_goal ctxt goal)
    4.62 +    else
    4.63 +      Seq.Error (fn () =>
    4.64 +        finished_goal_error ^ Position.here pos ^ ":\n" ^
    4.65 +          Proof_Display.string_of_goal ctxt goal)
    4.66    end;
    4.67  
    4.68  
    4.69 @@ -817,18 +820,25 @@
    4.70    Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
    4.71      method_error "initial" (Method.position arg));
    4.72  
    4.73 -fun end_proof bot (arg, immed) =
    4.74 -  Seq.APPEND (fn state =>
    4.75 -    state
    4.76 -    |> assert_forward
    4.77 -    |> assert_bottom bot
    4.78 -    |> close_block
    4.79 -    |> assert_current_goal true
    4.80 -    |> using_facts []
    4.81 -    |> `before_qed |-> (refine o the_default Method.succeed_text)
    4.82 -    |> Seq.maps (refine (Method.finish_text (Method.text arg, immed)))
    4.83 -    |> Seq.make_results, method_error "terminal" (Method.position arg))
    4.84 -  #> Seq.maps_results (Seq.single o finished_goal);
    4.85 +fun end_proof bot (prev_pos, (opt_text, immed)) =
    4.86 +  let
    4.87 +    val (finish_text, terminal_pos, finished_pos) =
    4.88 +      (case opt_text of
    4.89 +        NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
    4.90 +      | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
    4.91 +  in
    4.92 +    Seq.APPEND (fn state =>
    4.93 +      state
    4.94 +      |> assert_forward
    4.95 +      |> assert_bottom bot
    4.96 +      |> close_block
    4.97 +      |> assert_current_goal true
    4.98 +      |> using_facts []
    4.99 +      |> `before_qed |-> (refine o the_default Method.succeed_text)
   4.100 +      |> Seq.maps (refine finish_text)
   4.101 +      |> Seq.make_results, method_error "terminal" terminal_pos)
   4.102 +    #> Seq.maps_results (Seq.single o finished_goal finished_pos)
   4.103 +  end;
   4.104  
   4.105  fun check_result msg sq =
   4.106    (case Seq.pull sq of
   4.107 @@ -850,11 +860,11 @@
   4.108  
   4.109  fun apply_end text = assert_forward #> refine_end text;
   4.110  
   4.111 -fun apply_results (text, pos) =
   4.112 -  Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
   4.113 +fun apply_results (text, range) =
   4.114 +  Seq.APPEND (apply text #> Seq.make_results, method_error "" (Position.set_range range));
   4.115  
   4.116 -fun apply_end_results (text, pos) =
   4.117 -  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
   4.118 +fun apply_end_results (text, range) =
   4.119 +  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" (Position.set_range range));
   4.120  
   4.121  
   4.122  
   4.123 @@ -964,7 +974,8 @@
   4.124    #> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
   4.125      (fn ((after_qed, _), results) => after_qed results));
   4.126  
   4.127 -fun local_qed arg = local_qeds arg #> Seq.the_result finished_goal_error;
   4.128 +fun local_qed arg =
   4.129 +  local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
   4.130  
   4.131  
   4.132  (* global goals *)
   4.133 @@ -985,26 +996,27 @@
   4.134    #> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
   4.135      after_qed results (context_of state)));
   4.136  
   4.137 -fun global_qed arg = global_qeds arg #> Seq.the_result finished_goal_error;
   4.138 +fun global_qed arg =
   4.139 +  global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
   4.140  
   4.141  
   4.142  (* concluding steps *)
   4.143  
   4.144  fun terminal_proof qeds initial terminal =
   4.145 -  proof_results (SOME initial) #> Seq.maps_results (qeds terminal)
   4.146 +  proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
   4.147    #> Seq.the_result "";
   4.148  
   4.149  fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
   4.150 -val local_default_proof = local_terminal_proof ((Method.default_text, Position.none), NONE);
   4.151 -val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.none), NONE);
   4.152 -fun local_skip_proof int = local_terminal_proof ((Method.sorry_text int, Position.none), NONE);
   4.153 -val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.none) (NONE, false);
   4.154 +val local_default_proof = local_terminal_proof ((Method.default_text, Position.no_range), NONE);
   4.155 +val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.no_range), NONE);
   4.156 +fun local_skip_proof int = local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE);
   4.157 +val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.no_range) (NONE, false);
   4.158  
   4.159  fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
   4.160 -val global_default_proof = global_terminal_proof ((Method.default_text, Position.none), NONE);
   4.161 -val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.none), NONE);
   4.162 -fun global_skip_proof int = global_terminal_proof ((Method.sorry_text int, Position.none), NONE);
   4.163 -val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.none) (NONE, false);
   4.164 +val global_default_proof = global_terminal_proof ((Method.default_text, Position.no_range), NONE);
   4.165 +val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE);
   4.166 +fun global_skip_proof int = global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE);
   4.167 +val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false);
   4.168  
   4.169  
   4.170  (* common goal statements *)