--- a/src/HOL/IMP/Abs_Int3.thy Wed Oct 17 15:25:52 2012 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Wed Oct 17 22:45:40 2012 +0200
@@ -704,5 +704,6 @@
which is again not a pfp: not f 2 = 3 <= 2
Another widening step yields 2 widen f 2 = 2 widen 3 = 3
*)
+oops
end
--- a/src/HOL/Statespace/state_space.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Oct 17 22:45:40 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)), Position.none), NONE)
+ ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
|> Proof_Context.theory_of
fun add_locale name expr elems thy =
--- a/src/Pure/Concurrent/future.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Oct 17 22:45:40 2012 +0200
@@ -183,7 +183,9 @@
fun cancel_now group = (*requires SYNCHRONIZED*)
let
val running = Task_Queue.cancel (! queue) group;
- val _ = List.app Simple_Thread.interrupt_unsynchronized running;
+ val _ = running |> List.app (fn thread =>
+ if Simple_Thread.is_self thread then ()
+ else Simple_Thread.interrupt_unsynchronized thread);
in running end;
fun cancel_all () = (*requires SYNCHRONIZED*)
--- a/src/Pure/Concurrent/simple_thread.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML Wed Oct 17 22:45:40 2012 +0200
@@ -6,6 +6,7 @@
signature SIMPLE_THREAD =
sig
+ val is_self: Thread.thread -> bool
val attributes: bool -> Thread.threadAttribute list
val fork: bool -> (unit -> unit) -> Thread.thread
val interrupt_unsynchronized: Thread.thread -> unit
@@ -15,6 +16,8 @@
structure Simple_Thread: SIMPLE_THREAD =
struct
+fun is_self thread = Thread.equal (Thread.self (), thread);
+
fun attributes interrupts =
if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;
--- a/src/Pure/Isar/isar_cmd.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Oct 17 22:45:40 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_position option -> Toplevel.transition -> Toplevel.transition
- val terminal_proof: Method.text_position * Method.text_position option ->
+ val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
+ val terminal_proof: Method.text_range * Method.text_range option ->
Toplevel.transition -> Toplevel.transition
val default_proof: Toplevel.transition -> Toplevel.transition
val immediate_proof: Toplevel.transition -> Toplevel.transition
--- a/src/Pure/Isar/method.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Pure/Isar/method.ML Wed Oct 17 22:45:40 2012 +0200
@@ -73,10 +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
- 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
+ type text_range = text * Position.range
+ val parse: text_range parser
+ val text: text_range option -> text option
+ val position: text_range option -> Position.T
end;
structure Method: METHOD =
@@ -417,20 +417,20 @@
in
val parse =
- Scan.trace meth3 >> (fn (m, toks) => (m, Position.set_range (Token.position_range_of toks)));
+ Scan.trace meth3 >> (fn (m, toks) => (m, Token.position_range_of toks));
end;
(* text position *)
-type text_position = text * Position.T;
+type text_range = text * Position.range;
fun text NONE = NONE
| text (SOME (txt, _)) = SOME txt;
fun position NONE = Position.none
- | position (SOME (_, pos)) = pos;
+ | position (SOME (_, range)) = Position.set_range range;
(* theory setup *)
--- a/src/Pure/Isar/proof.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Pure/Isar/proof.ML Wed Oct 17 22:45:40 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_position option -> state -> state Seq.result Seq.seq
+ val proof_results: Method.text_range 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 apply_results: Method.text_range -> state -> state Seq.result Seq.seq
+ val apply_end_results: Method.text_range -> 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_position option * bool -> state -> state
+ val local_qed: Method.text_range 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_position option * bool -> state -> context
- val local_terminal_proof: Method.text_position * Method.text_position option -> state -> state
+ val global_qed: Method.text_range option * bool -> state -> context
+ val local_terminal_proof: Method.text_range * Method.text_range 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_position * Method.text_position option -> state -> context
+ val global_terminal_proof: Method.text_range * Method.text_range option -> state -> context
val global_default_proof: state -> context
val global_immediate_proof: state -> context
val global_skip_proof: bool -> state -> context
@@ -116,9 +116,9 @@
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_position * Method.text_position option -> bool ->
+ val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
state -> state
- val global_future_terminal_proof: Method.text_position * Method.text_position option -> bool ->
+ val global_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
state -> context
end;
@@ -508,10 +508,13 @@
val finished_goal_error = "Failed to finish proof";
-fun finished_goal state =
+fun finished_goal pos 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)
+ else
+ Seq.Error (fn () =>
+ finished_goal_error ^ Position.here pos ^ ":\n" ^
+ Proof_Display.string_of_goal ctxt goal)
end;
@@ -817,18 +820,25 @@
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 end_proof bot (prev_pos, (opt_text, immed)) =
+ let
+ val (finish_text, terminal_pos, finished_pos) =
+ (case opt_text of
+ NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
+ | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
+ in
+ 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 finish_text)
+ |> Seq.make_results, method_error "terminal" terminal_pos)
+ #> Seq.maps_results (Seq.single o finished_goal finished_pos)
+ end;
fun check_result msg sq =
(case Seq.pull sq of
@@ -850,11 +860,11 @@
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_results (text, range) =
+ Seq.APPEND (apply text #> Seq.make_results, method_error "" (Position.set_range range));
-fun apply_end_results (text, pos) =
- Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
+fun apply_end_results (text, range) =
+ Seq.APPEND (apply_end text #> Seq.make_results, method_error "" (Position.set_range range));
@@ -964,7 +974,8 @@
#> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
(fn ((after_qed, _), results) => after_qed results));
-fun local_qed arg = local_qeds arg #> Seq.the_result finished_goal_error;
+fun local_qed arg =
+ local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
(* global goals *)
@@ -985,26 +996,38 @@
#> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
after_qed results (context_of state)));
-fun global_qed arg = global_qeds arg #> Seq.the_result finished_goal_error;
+fun global_qed arg =
+ global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
(* concluding steps *)
+local
+
fun terminal_proof qeds initial terminal =
- proof_results (SOME initial) #> Seq.maps_results (qeds terminal)
+ proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
#> Seq.the_result "";
+fun skipped_proof x =
+ (Output.report (Markup.markup Isabelle_Markup.bad "Skipped proof"); x);
+
+in
+
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, 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);
+val local_default_proof = local_terminal_proof ((Method.default_text, Position.no_range), NONE);
+val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.no_range), NONE);
+fun local_skip_proof int =
+ local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) #> skipped_proof;
+val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.no_range) (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, 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);
+val global_default_proof = global_terminal_proof ((Method.default_text, Position.no_range), NONE);
+val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE);
+fun global_skip_proof int =
+ global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) #> skipped_proof;
+val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false);
+
+end;
(* common goal statements *)
--- a/src/Pure/Isar/proof_context.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Oct 17 22:45:40 2012 +0200
@@ -51,6 +51,7 @@
val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
val extern_fact: Proof.context -> string -> xstring
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
+ val markup_fact: Proof.context -> string -> Markup.T
val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
val pretty_fact: Proof.context -> string * thm list -> Pretty.T
val read_class: Proof.context -> xstring -> class
--- a/src/Pure/System/session.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Pure/System/session.ML Wed Oct 17 22:45:40 2012 +0200
@@ -72,6 +72,9 @@
Keyword.status ();
Outer_Syntax.check_syntax ();
Future.shutdown ();
+ Goal.finish_futures ();
+ Goal.cancel_futures ();
+ Future.shutdown ();
Options.reset_default ();
session_finished := true);
--- a/src/Pure/Tools/find_consts.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Pure/Tools/find_consts.ML Wed Oct 17 22:45:40 2012 +0200
@@ -55,12 +55,14 @@
| Name name => Pretty.str (prfx "name: " ^ quote name))
end;
-fun pretty_const ctxt (nm, ty) =
+fun pretty_const ctxt (c, ty) =
let
val ty' = Logic.unvarifyT_global ty;
+ val consts_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
+ val markup = Name_Space.markup consts_space c;
in
Pretty.block
- [Pretty.str nm, Pretty.str " ::", Pretty.brk 1,
+ [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt ty')]
end;
--- a/src/Pure/Tools/find_theorems.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Pure/Tools/find_theorems.ML Wed Oct 17 22:45:40 2012 +0200
@@ -554,12 +554,21 @@
val find_theorems = gen_find_theorems filter_theorems;
val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
-fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block
- [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
- Display.pretty_thm ctxt thm]
- | pretty_theorem ctxt (External (thmref, prop)) = Pretty.block
- [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
- Syntax.unparse_term ctxt prop];
+fun pretty_ref ctxt thmref =
+ let
+ val (name, sel) =
+ (case thmref of
+ Facts.Named ((name, _), sel) => (name, sel)
+ | Facts.Fact _ => raise Fail "Illegal literal fact");
+ in
+ [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
+ Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
+ end;
+
+fun pretty_theorem ctxt (Internal (thmref, thm)) =
+ Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm])
+ | pretty_theorem ctxt (External (thmref, prop)) =
+ Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]);
fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
--- a/src/Pure/facts.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Pure/facts.ML Wed Oct 17 22:45:40 2012 +0200
@@ -12,6 +12,7 @@
Named of (string * Position.T) * interval list option |
Fact of string
val named: string -> ref
+ val string_of_selection: interval list option -> string
val string_of_ref: ref -> string
val name_of_ref: ref -> string
val pos_of_ref: ref -> Position.T
@@ -77,7 +78,7 @@
fun named name = Named ((name, Position.none), NONE);
fun name_pos_of_ref (Named (name_pos, _)) = name_pos
- | name_pos_of_ref (Fact _) = error "Illegal literal fact";
+ | name_pos_of_ref (Fact _) = raise Fail "Illegal literal fact";
val name_of_ref = #1 o name_pos_of_ref;
val pos_of_ref = #2 o name_pos_of_ref;
@@ -85,10 +86,11 @@
fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
| map_name_of_ref _ r = r;
-fun string_of_ref (Named ((name, _), NONE)) = name
- | string_of_ref (Named ((name, _), SOME is)) =
- name ^ enclose "(" ")" (commas (map string_of_interval is))
- | string_of_ref (Fact _) = error "Illegal literal fact";
+fun string_of_selection NONE = ""
+ | string_of_selection (SOME is) = enclose "(" ")" (commas (map string_of_interval is));
+
+fun string_of_ref (Named ((name, _), sel)) = name ^ string_of_selection sel
+ | string_of_ref (Fact _) = raise Fail "Illegal literal fact";
(* select *)
--- a/src/Pure/goal.ML Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Pure/goal.ML Wed Oct 17 22:45:40 2012 +0200
@@ -27,6 +27,7 @@
val fork_name: string -> (unit -> 'a) -> 'a future
val fork: (unit -> 'a) -> 'a future
val peek_futures: serial -> unit future list
+ val finish_futures: unit -> unit
val cancel_futures: unit -> unit
val future_enabled_level: int -> bool
val future_enabled: unit -> bool
@@ -173,6 +174,11 @@
fun peek_futures id =
Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
+fun finish_futures () =
+ (case map_filter Task_Queue.group_status (#2 (Synchronized.value forked_proofs)) of
+ [] => ()
+ | exns => raise Par_Exn.make exns);
+
fun cancel_futures () =
Synchronized.change forked_proofs (fn (m, groups, tab) =>
(List.app Future.cancel_group groups; (0, [], Inttab.empty)));
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Oct 17 15:25:52 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed Oct 17 22:45:40 2012 +0200
@@ -169,6 +169,15 @@
}
update.tooltip = "Update display according to the command at cursor position"
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
+ private val detach = new Button("Detach") {
+ reactions += {
+ case ButtonClicked(_) =>
+ Info_Dockable(view, current_snapshot, Pretty.separate(current_output))
+ }
+ }
+ detach.tooltip = "Detach window with static copy of current output"
+
+ private val controls =
+ new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update, detach)
add(controls.peer, BorderLayout.NORTH)
}