--- a/src/HOL/HOLCF/IOA/ABP/Check.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/HOLCF/IOA/ABP/Check.ML Tue Aug 23 15:46:53 2011 -0700
@@ -112,21 +112,21 @@
------------------------------------*)
fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
- let fun prec x = (Output.raw_stdout ","; pre x)
+ let fun prec x = (Output.physical_stdout ","; pre x)
in
(case lll of
- [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
- | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
+ [] => (Output.physical_stdout lpar; Output.physical_stdout rpar)
+ | x::lll => (Output.physical_stdout lpar; pre x; List.app prec lll; Output.physical_stdout rpar))
end;
-fun pr_bool true = Output.raw_stdout "true"
-| pr_bool false = Output.raw_stdout "false";
+fun pr_bool true = Output.physical_stdout "true"
+| pr_bool false = Output.physical_stdout "false";
-fun pr_msg m = Output.raw_stdout "m"
-| pr_msg n = Output.raw_stdout "n"
-| pr_msg l = Output.raw_stdout "l";
+fun pr_msg m = Output.physical_stdout "m"
+| pr_msg n = Output.physical_stdout "n"
+| pr_msg l = Output.physical_stdout "l";
-fun pr_act a = Output.raw_stdout (case a of
+fun pr_act a = Output.physical_stdout (case a of
Next => "Next"|
S_msg(ma) => "S_msg(ma)" |
R_msg(ma) => "R_msg(ma)" |
@@ -135,17 +135,17 @@
S_ack(b) => "S_ack(b)" |
R_ack(b) => "R_ack(b)");
-fun pr_pkt (b,ma) = (Output.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
+fun pr_pkt (b,ma) = (Output.physical_stdout "<"; pr_bool b;Output.physical_stdout ", "; pr_msg ma; Output.physical_stdout ">");
val pr_bool_list = print_list("[","]",pr_bool);
val pr_msg_list = print_list("[","]",pr_msg);
val pr_pkt_list = print_list("[","]",pr_pkt);
fun pr_tuple (env,p,a,q,b,ch1,ch2) =
- (Output.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p; Output.raw_stdout ", ";
- pr_bool a; Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", ";
- pr_bool b; Output.raw_stdout ", "; pr_pkt_list ch1; Output.raw_stdout ", ";
- pr_bool_list ch2; Output.raw_stdout "}");
+ (Output.physical_stdout "{"; pr_bool env; Output.physical_stdout ", "; pr_msg_list p; Output.physical_stdout ", ";
+ pr_bool a; Output.physical_stdout ", "; pr_msg_list q; Output.physical_stdout ", ";
+ pr_bool b; Output.physical_stdout ", "; pr_pkt_list ch1; Output.physical_stdout ", ";
+ pr_bool_list ch2; Output.physical_stdout "}");
--- a/src/HOL/Library/FuncSet.thy Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/Library/FuncSet.thy Tue Aug 23 15:46:53 2011 -0700
@@ -72,7 +72,7 @@
by (auto simp: Pi_def)
lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
- by (auto intro: Pi_I)
+ by auto
lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
by (simp add: Pi_def)
@@ -257,7 +257,7 @@
where "extensional_funcset S T = (S -> T) \<inter> (extensional S)"
lemma extensional_empty[simp]: "extensional {} = {%x. undefined}"
-unfolding extensional_def by (auto intro: ext)
+unfolding extensional_def by auto
lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}"
unfolding extensional_funcset_def by simp
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 23 15:46:53 2011 -0700
@@ -15,11 +15,14 @@
val e_weight_methodK = "e_weight_method"
val force_sosK = "force_sos"
val max_relevantK = "max_relevant"
+val max_callsK = "max_calls"
val minimizeK = "minimize"
val minimize_timeoutK = "minimize_timeout"
val metis_ftK = "metis_ft"
val reconstructorK = "reconstructor"
+val preplay_timeout = "4"
+
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
fun reconstructor_tag reconstructor id =
@@ -361,7 +364,7 @@
fun set_file_name (SOME dir) =
Config.put Sledgehammer_Provers.dest_dir dir
#> Config.put Sledgehammer_Provers.problem_prefix
- ("prob_" ^ str0 (Position.line_of pos))
+ ("prob_" ^ str0 (Position.line_of pos) ^ "__")
#> Config.put SMT_Config.debug_files
(dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
^ serial_string ())
@@ -376,15 +379,18 @@
e_weight_method |> the_default I)
#> (Option.map (Config.put ATP_Systems.force_sos)
force_sos |> the_default I)
- #> Config.put Sledgehammer_Provers.measure_run_time true)
+ #> Config.put Sledgehammer_Provers.measure_run_time true
+ #> Config.put Sledgehammer_Provers.atp_sound_modulo_infiniteness false)
val params as {relevance_thresholds, max_relevant, slicing, ...} =
Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),
("type_enc", type_enc),
("sound", sound),
+ ("preplay_timeout", preplay_timeout),
("max_relevant", max_relevant),
("slicing", slicing),
- ("timeout", string_of_int timeout)]
+ ("timeout", string_of_int timeout),
+ ("preplay_timeout", preplay_timeout)]
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
prover_name
@@ -520,7 +526,8 @@
("verbose", "true"),
("type_enc", type_enc),
("sound", sound),
- ("timeout", string_of_int timeout)]
+ ("timeout", string_of_int timeout),
+ ("preplay_timeout", preplay_timeout)]
val minimize =
Sledgehammer_Minimize.minimize_facts prover_name params
true 1 (Sledgehammer_Util.subgoal_count st)
@@ -543,6 +550,20 @@
end
+val e_override_params =
+ [("provers", "e"),
+ ("max_relevant", "0"),
+ ("type_enc", "poly_guards?"),
+ ("sound", "true"),
+ ("slicing", "false")]
+
+val vampire_override_params =
+ [("provers", "vampire"),
+ ("max_relevant", "0"),
+ ("type_enc", "poly_tags"),
+ ("sound", "true"),
+ ("slicing", "false")]
+
fun run_reconstructor trivial full m name reconstructor named_thms id
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
let
@@ -550,15 +571,21 @@
(if !reconstructor = "sledgehammer_tac" then
(fn ctxt => fn thms =>
Method.insert_tac thms THEN'
- Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)
+ (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+ e_override_params
+ ORELSE'
+ Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+ vampire_override_params))
else if !reconstructor = "smt" then
SMT_Solver.smt_tac
else if full orelse !reconstructor = "metis (full_types)" then
Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc]
else if !reconstructor = "metis (no_types)" then
Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
+ else if !reconstructor = "metis" then
+ Metis_Tactics.metis_tac []
else
- Metis_Tactics.metis_tac []) ctxt thms
+ K (K (K all_tac))) ctxt thms
fun apply_reconstructor thms =
Mirabelle.can_apply timeout (do_reconstructor thms) st
@@ -591,48 +618,60 @@
val try_timeout = seconds 5.0
+(* crude hack *)
+val num_sledgehammer_calls = Unsynchronized.ref 0
+
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
then () else
let
- val reconstructor = Unsynchronized.ref ""
- val named_thms =
- Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
- val minimize = AList.defined (op =) args minimizeK
- val metis_ft = AList.defined (op =) args metis_ftK
- val trivial =
- Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre
- handle TimeLimit.TimeOut => false
- fun apply_reconstructor m1 m2 =
- if metis_ft
- then
- if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false
- (run_reconstructor trivial false m1 name reconstructor
- (these (!named_thms))) id st)
+ val max_calls =
+ AList.lookup (op =) args max_callsK |> the_default "10000000"
+ |> Int.fromString |> the
+ val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1;
+ in
+ if !num_sledgehammer_calls > max_calls then ()
+ else
+ let
+ val reconstructor = Unsynchronized.ref ""
+ val named_thms =
+ Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
+ val minimize = AList.defined (op =) args minimizeK
+ val metis_ft = AList.defined (op =) args metis_ftK
+ val trivial =
+ Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre
+ handle TimeLimit.TimeOut => false
+ fun apply_reconstructor m1 m2 =
+ if metis_ft
+ then
+ if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+ (run_reconstructor trivial false m1 name reconstructor
+ (these (!named_thms))) id st)
+ then
+ (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+ (run_reconstructor trivial true m2 name reconstructor
+ (these (!named_thms))) id st; ())
+ else ()
+ else
+ (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+ (run_reconstructor trivial false m1 name reconstructor
+ (these (!named_thms))) id st; ())
+ in
+ change_data id (set_mini minimize);
+ Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor
+ named_thms) id st;
+ if is_some (!named_thms)
then
- (Mirabelle.catch_result (reconstructor_tag reconstructor) false
- (run_reconstructor trivial true m2 name reconstructor
- (these (!named_thms))) id st; ())
+ (apply_reconstructor Unminimized UnminimizedFT;
+ if minimize andalso not (null (these (!named_thms)))
+ then
+ (Mirabelle.catch minimize_tag
+ (run_minimize args reconstructor named_thms) id st;
+ apply_reconstructor Minimized MinimizedFT)
+ else ())
else ()
- else
- (Mirabelle.catch_result (reconstructor_tag reconstructor) false
- (run_reconstructor trivial false m1 name reconstructor
- (these (!named_thms))) id st; ())
- in
- change_data id (set_mini minimize);
- Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor
- named_thms) id st;
- if is_some (!named_thms)
- then
- (apply_reconstructor Unminimized UnminimizedFT;
- if minimize andalso not (null (these (!named_thms)))
- then
- (Mirabelle.catch minimize_tag
- (run_minimize args reconstructor named_thms) id st;
- apply_reconstructor Minimized MinimizedFT)
- else ())
- else ()
+ end
end
end
--- a/src/HOL/TPTP/CASC_Setup.thy Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/TPTP/CASC_Setup.thy Tue Aug 23 15:46:53 2011 -0700
@@ -119,14 +119,14 @@
SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
ORELSE
SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
- (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
+ (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
ORELSE
SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
- THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
+ THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "metis"
(ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 23 15:46:53 2011 -0700
@@ -270,7 +270,7 @@
(* SPASS *)
(* The "-VarWeight=3" option helps the higher-order problems, probably by
- counteracting the presence of "hAPP". *)
+ counteracting the presence of explicit application operators. *)
val spass_config : atp_config =
{exec = ("ISABELLE_ATP", "scripts/spass"),
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
@@ -334,12 +334,13 @@
prem_kind = Conjecture,
best_slices = fn ctxt =>
(* FUDGE *)
- (0.333, (false, (150, FOF, "poly_guards", sosN))) ::
(if is_old_vampire_version () then
- [(0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
+ [(0.333, (false, (150, FOF, "poly_guards", sosN))),
+ (0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
(0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
else
- [(0.334, (true, (50, TFF, "simple", no_sosN))),
+ [(0.333, (false, (150, TFF, "poly_guards", sosN))),
+ (0.334, (true, (50, TFF, "simple", no_sosN))),
(0.333, (false, (500, TFF, "simple", sosN)))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 23 15:46:53 2011 -0700
@@ -165,8 +165,8 @@
val untyped_helper_suffix = "_U"
val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
-val predicator_name = "hBOOL"
-val app_op_name = "hAPP"
+val predicator_name = "p"
+val app_op_name = "a"
val type_guard_name = "g"
val type_tag_name = "t"
val simple_type_prefix = "ty_"
@@ -1151,7 +1151,7 @@
| homo _ _ = raise Fail "expected function type"
in homo end
-(** "hBOOL" and "hAPP" **)
+(** predicators and application operators **)
type sym_info =
{pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
@@ -1194,6 +1194,8 @@
if String.isPrefix bound_var_prefix s orelse
String.isPrefix all_bound_var_prefix s then
add_universal_var T accum
+ else if String.isPrefix exist_bound_var_prefix s then
+ accum
else
let val ary = length args in
((bool_vars, fun_var_Ts),
@@ -1238,8 +1240,8 @@
end
in add true end
fun add_fact_syms_to_table ctxt explicit_apply =
- fact_lift (formula_fold NONE
- (K (add_iterm_syms_to_table ctxt explicit_apply)))
+ formula_fold NONE (K (add_iterm_syms_to_table ctxt explicit_apply))
+ |> fact_lift
val tvar_a = TVar (("'a", 0), HOLogic.typeS)
@@ -1379,6 +1381,9 @@
(** Helper facts **)
+val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
+val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
+
(* The Boolean indicates that a fairly sound type encoding is needed. *)
val helper_table =
[(("COMBI", false), @{thms Meson.COMBI_def}),
@@ -1386,9 +1391,10 @@
(("COMBB", false), @{thms Meson.COMBB_def}),
(("COMBC", false), @{thms Meson.COMBC_def}),
(("COMBS", false), @{thms Meson.COMBS_def}),
- (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
+ ((predicator_name, false), [not_ffalse, ftrue]),
+ (("fFalse", false), [not_ffalse]),
(("fFalse", true), @{thms True_or_False}),
- (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
+ (("fTrue", false), [ftrue]),
(("fTrue", true), @{thms True_or_False}),
(("fNot", false),
@{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
@@ -1754,9 +1760,7 @@
(case type_enc of
Guards _ => not pred_sym
| _ => true) andalso
- is_tptp_user_symbol s andalso
- forall (fn prefix => not (String.isPrefix prefix s))
- [bound_var_prefix, all_bound_var_prefix, exist_bound_var_prefix]
+ is_tptp_user_symbol s
fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
(conjs, facts) =
--- a/src/HOL/ex/Unification.thy Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/ex/Unification.thy Tue Aug 23 15:46:53 2011 -0700
@@ -11,10 +11,10 @@
begin
text {*
- Implements Manna & Waldinger's formalization, with Paulson's
+ Implements Manna \& Waldinger's formalization, with Paulson's
simplifications, and some new simplifications by Slind and Krauss.
- Z Manna & R Waldinger, Deductive Synthesis of the Unification
+ Z Manna \& R Waldinger, Deductive Synthesis of the Unification
Algorithm. SCP 1 (1981), 5-48
L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5
--- a/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 23 15:46:53 2011 -0700
@@ -7,22 +7,21 @@
signature SLEDGEHAMMER_TACTICS =
sig
- val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
- val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
- val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
+ val sledgehammer_with_metis_tac :
+ Proof.context -> (string * string) list -> int -> tactic
+ val sledgehammer_as_oracle_tac :
+ Proof.context -> (string * string) list -> int -> tactic
end;
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
struct
-fun run_atp force_full_types timeout i n ctxt goal name =
+fun run_atp override_params i n ctxt goal =
let
val chained_ths = [] (* a tactic has no chained ths *)
- val params as {relevance_thresholds, max_relevant, slicing, ...} =
- ((if force_full_types then [("sound", "true")] else [])
- @ [("timeout", string_of_int (Time.toSeconds timeout))])
- (* @ [("overlord", "true")] *)
- |> Sledgehammer_Isar.default_params ctxt
+ val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
+ Sledgehammer_Isar.default_params ctxt override_params
+ val name = hd provers
val prover =
Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
val default_max_relevant =
@@ -50,8 +49,6 @@
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
end
-val atp = "e" (* or "vampire" or "spass" etc. *)
-
fun thms_of_name ctxt name =
let
val lex = Keyword.get_lexicons
@@ -65,25 +62,16 @@
|> Source.exhaust
end
-fun sledgehammer_with_metis_tac ctxt i th =
- let
- val timeout = Time.fromSeconds 30
- in
- case run_atp false timeout i i ctxt th atp of
- SOME facts =>
- Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
- | NONE => Seq.empty
- end
+fun sledgehammer_with_metis_tac ctxt override_params i th =
+ case run_atp override_params i i ctxt th of
+ SOME facts =>
+ Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
+ | NONE => Seq.empty
-fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
+fun sledgehammer_as_oracle_tac ctxt override_params i th =
let
val thy = Proof_Context.theory_of ctxt
- val timeout = Time.fromSeconds 30
- val xs = run_atp force_full_types timeout i i ctxt th atp
+ val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th
in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
-val sledgehammer_as_unsound_oracle_tac =
- generic_sledgehammer_as_oracle_tac false
-val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
-
end;
--- a/src/Pure/Concurrent/future.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Concurrent/future.ML Tue Aug 23 15:46:53 2011 -0700
@@ -51,13 +51,12 @@
val task_of: 'a future -> task
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
- val get_finished: 'a future -> 'a
val interruptible_task: ('a -> 'b) -> 'a -> 'b
val cancel_group: group -> task list
val cancel: 'a future -> task list
- type fork_params =
- {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
- val forks: fork_params -> (unit -> 'a) list -> 'a future list
+ type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
+ val default_params: params
+ val forks: params -> (unit -> 'a) list -> 'a future list
val fork_pri: int -> (unit -> 'a) -> 'a future
val fork: (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
@@ -67,7 +66,7 @@
val join_tasks: task list -> unit
val value_result: 'a Exn.result -> 'a future
val value: 'a -> 'a future
- val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
+ val cond_forks: params -> (unit -> 'a) list -> 'a future list
val map: ('a -> 'b) -> 'a future -> 'b future
val promise_group: group -> (unit -> unit) -> 'a future
val promise: (unit -> unit) -> 'a future
@@ -125,11 +124,6 @@
fun peek x = Single_Assignment.peek (result_of x);
fun is_finished x = is_some (peek x);
-fun get_finished x =
- (case peek x of
- SOME res => Exn.release res
- | NONE => raise Fail "Unfinished future evaluation");
-
(** scheduling **)
@@ -464,10 +458,10 @@
(* fork *)
-type fork_params =
- {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
+type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
+val default_params: params = {name = "", group = NONE, deps = [], pri = 0, interrupts = true};
-fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
+fun forks ({name, group, deps, pri, interrupts}: params) es =
if null es then []
else
let
--- a/src/Pure/Concurrent/lazy.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Concurrent/lazy.ML Tue Aug 23 15:46:53 2011 -0700
@@ -11,11 +11,12 @@
type 'a lazy
val peek: 'a lazy -> 'a Exn.result option
val is_finished: 'a lazy -> bool
- val get_finished: 'a lazy -> 'a
val lazy: (unit -> 'a) -> 'a lazy
val value: 'a -> 'a lazy
val force_result: 'a lazy -> 'a Exn.result
val force: 'a lazy -> 'a
+ val map: ('a -> 'b) -> 'a lazy -> 'b lazy
+ val future: Future.params -> 'a lazy -> 'a future
end;
structure Lazy: LAZY =
@@ -40,11 +41,6 @@
fun is_finished x = is_some (peek x);
-fun get_finished x =
- (case peek x of
- SOME res => Exn.release res
- | NONE => raise Fail "Unfinished lazy evaluation");
-
(* force result *)
@@ -77,9 +73,19 @@
| NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
end) ());
-fun force r = Exn.release (force_result r);
end;
+
+fun force r = Exn.release (force_result r);
+fun map f x = lazy (fn () => f (force x));
+
+
+(* future evaluation *)
+
+fun future params x =
+ if is_finished x then Future.value_result (force_result x)
+ else (singleton o Future.forks) params (fn () => force x);
+
end;
type 'a lazy = 'a Lazy.lazy;
--- a/src/Pure/Concurrent/lazy_sequential.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Concurrent/lazy_sequential.ML Tue Aug 23 15:46:53 2011 -0700
@@ -27,11 +27,6 @@
fun is_finished x = is_some (peek x);
-fun get_finished x =
- (case peek x of
- SOME res => Exn.release res
- | NONE => raise Fail "Unfinished lazy evaluation");
-
(* force result *)
@@ -45,6 +40,14 @@
in result end;
fun force r = Exn.release (force_result r);
+fun map f x = lazy (fn () => f (force x));
+
+
+(* future evaluation *)
+
+fun future params x =
+ if is_finished x then Future.value_result (force_result x)
+ else (singleton o Future.forks) params (fn () => force x);
end;
end;
--- a/src/Pure/General/output.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/General/output.ML Tue Aug 23 15:46:53 2011 -0700
@@ -22,9 +22,9 @@
val output_width: string -> output * int
val output: string -> output
val escape: output -> string
- val raw_stdout: output -> unit
- val raw_stderr: output -> unit
- val raw_writeln: output -> unit
+ val physical_stdout: output -> unit
+ val physical_stderr: output -> unit
+ val physical_writeln: output -> unit
structure Private_Hooks:
sig
val writeln_fn: (output -> unit) Unsynchronized.ref
@@ -78,24 +78,24 @@
(* raw output primitives -- not to be used in user-space *)
-fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
-fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
+fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
-fun raw_writeln "" = ()
- | raw_writeln s = raw_stdout (suffix "\n" s); (*atomic output!*)
+fun physical_writeln "" = ()
+ | physical_writeln s = physical_stdout (suffix "\n" s); (*atomic output!*)
(* Isabelle output channels *)
structure Private_Hooks =
struct
- val writeln_fn = Unsynchronized.ref raw_writeln;
+ val writeln_fn = Unsynchronized.ref physical_writeln;
val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
- val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
+ val warning_fn = Unsynchronized.ref (physical_stdout o suffix "\n" o prefix_lines "### ");
val error_fn =
- Unsynchronized.ref (fn (_: serial, s) => raw_stdout (suffix "\n" (prefix_lines "*** " s)));
- val prompt_fn = Unsynchronized.ref raw_stdout;
+ Unsynchronized.ref (fn (_: serial, s) => physical_stdout (suffix "\n" (prefix_lines "*** " s)));
+ val prompt_fn = Unsynchronized.ref physical_stdout;
val status_fn = Unsynchronized.ref (fn _: output => ());
val report_fn = Unsynchronized.ref (fn _: output => ());
val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
--- a/src/Pure/PIDE/command.scala Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/command.scala Tue Aug 23 15:46:53 2011 -0700
@@ -84,6 +84,19 @@
def span(toks: List[Token]): Command =
new Command(Document.no_id, toks)
+
+
+ /* perspective */
+
+ type Perspective = List[Command] // visible commands in canonical order
+
+ def equal_perspective(p1: Perspective, p2: Perspective): Boolean =
+ {
+ require(p1.forall(_.is_defined))
+ require(p2.forall(_.is_defined))
+ p1.length == p2.length &&
+ (p1.iterator zip p2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
+ }
}
@@ -93,12 +106,12 @@
{
/* classification */
+ def is_defined: Boolean = id != Document.no_id
+
def is_command: Boolean = !span.isEmpty && span.head.is_command
def is_ignored: Boolean = span.forall(_.is_ignored)
def is_malformed: Boolean = !is_command && !is_ignored
- def is_unparsed = id == Document.no_id
-
def name: String = if (is_command) span.head.content else ""
override def toString =
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
--- a/src/Pure/PIDE/document.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/document.ML Tue Aug 23 15:46:53 2011 -0700
@@ -19,7 +19,8 @@
datatype node_edit =
Clear |
Edits of (command_id option * command_id option) list |
- Header of node_header
+ Header of node_header |
+ Perspective of command_id list
type edit = string * node_edit
type state
val init_state: state
@@ -56,34 +57,54 @@
(** document structure **)
type node_header = (string * string list * (string * bool) list) Exn.result;
+type perspective = (command_id -> bool) * command_id list; (*visible commands, canonical order*)
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
abstype node = Node of
{header: node_header,
+ perspective: perspective,
entries: exec_id option Entries.T, (*command entries with excecutions*)
result: Toplevel.state lazy}
and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-fun make_node (header, entries, result) =
- Node {header = header, entries = entries, result = result};
+fun make_node (header, perspective, entries, result) =
+ Node {header = header, perspective = perspective, entries = entries, result = result};
+
+fun map_node f (Node {header, perspective, entries, result}) =
+ make_node (f (header, perspective, entries, result));
-fun map_node f (Node {header, entries, result}) =
- make_node (f (header, entries, result));
+val no_perspective: perspective = (K false, []);
+val no_print = Lazy.value ();
+val no_result = Lazy.value Toplevel.toplevel;
+
+val empty_node =
+ make_node (Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
+
+val clear_node =
+ map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_result));
+
+
+(* basic components *)
fun get_header (Node {header, ...}) = header;
-fun set_header header = map_node (fn (_, entries, result) => (header, entries, result));
+fun set_header header =
+ map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
-fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result);
+fun get_perspective (Node {perspective, ...}) = perspective;
+fun set_perspective perspective =
+ let val pred = Inttab.defined (Inttab.make (map (rpair ()) perspective)) in
+ map_node (fn (header, _, entries, result) => (header, (pred, perspective), entries, result))
+ end;
+
+fun map_entries f (Node {header, perspective, entries, result}) =
+ make_node (header, perspective, f entries, result);
fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
-fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result);
-fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
-
-val empty_exec = Lazy.value Toplevel.toplevel;
-val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec);
-val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
+fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
+fun set_result result =
+ map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
fun default_node name = Graph.default_node (name, empty_node);
@@ -95,7 +116,8 @@
datatype node_edit =
Clear |
Edits of (command_id option * command_id option) list |
- Header of node_header;
+ Header of node_header |
+ Perspective of command_id list;
type edit = string * node_edit;
@@ -150,7 +172,9 @@
val (header', nodes3) =
(header, Graph.add_deps_acyclic (name, parents) nodes2)
handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
- in Graph.map_node name (set_header header') nodes3 end));
+ in Graph.map_node name (set_header header') nodes3 end
+ | Perspective perspective =>
+ update_node name (set_perspective perspective) nodes));
fun put_node (name, node) (Version nodes) =
Version (update_node name (K node) nodes);
@@ -164,7 +188,8 @@
abstype state = State of
{versions: version Inttab.table, (*version_id -> document content*)
commands: Toplevel.transition future Inttab.table, (*command_id -> transition (future parsing)*)
- execs: Toplevel.state lazy Inttab.table, (*exec_id -> execution process*)
+ execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
+ (*exec_id -> command_id with eval/print process*)
execution: Future.group} (*global execution process*)
with
@@ -177,7 +202,7 @@
val init_state =
make_state (Inttab.make [(no_id, empty_version)],
Inttab.make [(no_id, Future.value Toplevel.empty)],
- Inttab.make [(no_id, empty_exec)],
+ Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
Future.new_group NONE);
@@ -252,14 +277,9 @@
SOME prf => Toplevel.status tr (Proof.status_markup prf)
| NONE => ());
-fun async_state tr st =
- (singleton o Future.forks)
- {name = "Document.async_state", group = SOME (Future.new_group NONE),
- deps = [], pri = 0, interrupts = true}
- (fn () =>
- Toplevel.setmp_thread_position tr
- (fn () => Toplevel.print_state false st) ())
- |> ignore;
+fun print_state tr st =
+ (Lazy.lazy o Toplevel.setmp_thread_position tr)
+ (fn () => Toplevel.print_state false st);
fun run int tr st =
(case Toplevel.transition int tr st of
@@ -286,12 +306,11 @@
val _ = List.app (Toplevel.error_msg tr) errs;
in
(case result of
- NONE => (Toplevel.status tr Markup.failed; st)
+ NONE => (Toplevel.status tr Markup.failed; (st, no_print))
| SOME st' =>
(Toplevel.status tr Markup.finished;
proof_status tr st';
- if do_print then async_state tr st' else ();
- st'))
+ (st', if do_print then print_state tr st' else no_print)))
end;
end;
@@ -313,13 +332,10 @@
fun new_exec (command_id, command) (assigns, execs, exec) =
let
val exec_id' = new_id ();
- val exec' =
- Lazy.lazy (fn () =>
- let
- val tr = Toplevel.put_id (print_id exec_id') (Future.get_finished command);
- val st = Lazy.get_finished exec;
- in run_command tr st end);
- in ((command_id, exec_id') :: assigns, (exec_id', exec') :: execs, exec') end;
+ val exec' = exec |> Lazy.map (fn (st, _) =>
+ let val tr = Toplevel.put_id (print_id exec_id') (Future.join command)
+ in run_command tr st end);
+ in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end;
in
@@ -351,7 +367,7 @@
| NONE =>
get_theory (Position.file_only import)
(#2 (Future.join (the (AList.lookup (op =) deps import))))));
- in Thy_Load.begin_theory dir thy_name imports files parents end
+ in Thy_Load.begin_theory dir thy_name imports files parents end;
fun get_command id =
(id, the_command state id |> Future.map (Toplevel.modify_init init));
in
@@ -364,12 +380,12 @@
(case prev of
NONE => no_id
| SOME prev_id => the_default no_id (the_entry node prev_id));
- val (assigns, execs, result) =
+ val (assigns, execs, last_exec) =
fold_entries (SOME id) (new_exec o get_command o #2 o #1)
- node ([], [], the_exec state prev_exec);
+ node ([], [], #2 (the_exec state prev_exec));
val node' = node
|> fold update_entry assigns
- |> set_result result;
+ |> set_result (Lazy.map #1 last_exec);
in ((assigns, execs, [(name, node')]), node') end)
end))
|> Future.joins |> map #1;
@@ -390,8 +406,17 @@
let
val version = the_version state version_id;
- fun force_exec NONE = ()
- | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
+ fun force_exec _ NONE = ()
+ | force_exec node (SOME exec_id) =
+ let
+ val (command_id, exec) = the_exec state exec_id;
+ val (_, print) = Lazy.force exec;
+ val perspective = get_perspective node;
+ val _ =
+ if #1 (get_perspective node) command_id orelse true (* FIXME *)
+ then ignore (Lazy.future Future.default_params print)
+ else ();
+ in () end;
val execution = Future.new_group NONE;
val _ =
@@ -400,7 +425,7 @@
(singleton o Future.forks)
{name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
- (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
+ (fold_entries NONE (fn (_, exec) => fn () => force_exec node exec) node));
in (versions, commands, execs, execution) end);
--- a/src/Pure/PIDE/document.scala Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/document.scala Tue Aug 23 15:46:53 2011 -0700
@@ -31,35 +31,37 @@
/* named nodes -- development graph */
- type Edit[A] = (String, Node.Edit[A])
- type Edit_Text = Edit[Text.Edit]
- type Edit_Command = Edit[(Option[Command], Option[Command])]
- type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
+ type Edit[A, B] = (String, Node.Edit[A, B])
+ type Edit_Text = Edit[Text.Edit, Text.Perspective]
+ type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
type Node_Header = Exn.Result[Thy_Header]
object Node
{
- sealed abstract class Edit[A]
+ sealed abstract class Edit[A, B]
{
- def map[B](f: A => B): Edit[B] =
+ def foreach(f: A => Unit)
+ {
this match {
- case Clear() => Clear()
- case Edits(es) => Edits(es.map(f))
- case Header(header) => Header(header)
+ case Edits(es) => es.foreach(f)
+ case _ =>
}
+ }
}
- case class Clear[A]() extends Edit[A]
- case class Edits[A](edits: List[A]) extends Edit[A]
- case class Header[A](header: Node_Header) extends Edit[A]
+ case class Clear[A, B]() extends Edit[A, B]
+ case class Edits[A, B](edits: List[A]) extends Edit[A, B]
+ case class Header[A, B](header: Node_Header) extends Edit[A, B]
+ case class Perspective[A, B](perspective: B) extends Edit[A, B]
- def norm_header[A](f: String => String, g: String => String, header: Node_Header): Header[A] =
+ def norm_header[A, B](f: String => String, g: String => String, header: Node_Header)
+ : Header[A, B] =
header match {
- case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f, g) })
- case exn => Header[A](exn)
+ case Exn.Res(h) => Header[A, B](Exn.capture { h.norm_deps(f, g) })
+ case exn => Header[A, B](exn)
}
- val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set())
+ val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
: Iterator[(Command, Text.Offset)] =
@@ -77,6 +79,7 @@
sealed case class Node(
val header: Node_Header,
+ val perspective: Command.Perspective,
val blobs: Map[String, Blob],
val commands: Linear_Set[Command])
{
--- a/src/Pure/PIDE/isar_document.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/isar_document.ML Tue Aug 23 15:46:53 2011 -0700
@@ -27,7 +27,8 @@
fn ([], a) =>
Document.Header
(Exn.Res (triple string (list string) (list (pair string bool)) a)),
- fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
+ fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
+ fn (a, []) => Document.Perspective (map int_atom a)]))
end;
val running = Document.cancel_execution state;
--- a/src/Pure/PIDE/isar_document.scala Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/isar_document.scala Tue Aug 23 15:46:53 2011 -0700
@@ -140,18 +140,20 @@
/* document versions */
def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
- edits: List[Document.Edit_Command_ID])
+ edits: List[Document.Edit_Command])
{
val edits_yxml =
{ import XML.Encode._
- def encode: T[List[Document.Edit_Command_ID]] =
+ def id: T[Command] = (cmd => long(cmd.id))
+ def encode: T[List[Document.Edit_Command]] =
list(pair(string,
variant(List(
{ case Document.Node.Clear() => (Nil, Nil) },
- { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
+ { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
{ case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
(Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
- { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
+ { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
+ { case Document.Node.Perspective(cs) => (cs.map(c => long_atom(c.id)), Nil) }))))
YXML.string_of_body(encode(edits)) }
input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
--- a/src/Pure/PIDE/markup_tree.scala Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/markup_tree.scala Tue Aug 23 15:46:53 2011 -0700
@@ -22,10 +22,7 @@
type Entry = (Text.Info[Any], Markup_Tree)
type T = SortedMap[Text.Range, Entry]
- val empty = SortedMap.empty[Text.Range, Entry](new scala.math.Ordering[Text.Range]
- {
- def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
- })
+ val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
def single(entry: Entry): T = update(empty, entry)
--- a/src/Pure/PIDE/text.scala Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/text.scala Tue Aug 23 15:46:53 2011 -0700
@@ -8,6 +8,11 @@
package isabelle
+import scala.collection.mutable
+import scala.math.Ordering
+import scala.util.Sorting
+
+
object Text
{
/* offset */
@@ -20,6 +25,11 @@
object Range
{
def apply(start: Offset): Range = Range(start, start)
+
+ object Ordering extends scala.math.Ordering[Text.Range]
+ {
+ def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
+ }
}
sealed case class Range(val start: Offset, val stop: Offset)
@@ -50,6 +60,33 @@
}
+ /* perspective */
+
+ type Perspective = List[Range] // visible text partitioning in canonical order
+
+ def perspective(ranges: Seq[Range]): Perspective =
+ {
+ val sorted_ranges = ranges.toArray
+ Sorting.quickSort(sorted_ranges)(Range.Ordering)
+
+ val result = new mutable.ListBuffer[Text.Range]
+ var last: Option[Text.Range] = None
+ for (range <- sorted_ranges)
+ {
+ last match {
+ case Some(last_range)
+ if ((last_range overlaps range) || last_range.stop == range.start) =>
+ last = Some(Text.Range(last_range.start, range.stop))
+ case _ =>
+ result ++= last
+ last = Some(range)
+ }
+ }
+ result ++= last
+ result.toList
+ }
+
+
/* information associated with text range */
sealed case class Info[A](val range: Text.Range, val info: A)
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Aug 23 15:46:53 2011 -0700
@@ -75,7 +75,7 @@
fun message bg en prfx text =
(case render text of
"" => ()
- | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
+ | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
fun setup_messages () =
(Output.Private_Hooks.writeln_fn := message "" "" "";
@@ -85,7 +85,7 @@
Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
- Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
+ Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
fun panic s =
(message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Aug 23 15:46:53 2011 -0700
@@ -66,7 +66,7 @@
fun matching_pgip_id id = (id = ! pgip_id)
-val output_xml_fn = Unsynchronized.ref Output.raw_writeln
+val output_xml_fn = Unsynchronized.ref Output.physical_writeln
fun output_xml s = ! output_xml_fn (XML.string_of s);
val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
@@ -1009,7 +1009,7 @@
(** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
local
- val pgip_output_channel = Unsynchronized.ref Output.raw_writeln
+ val pgip_output_channel = Unsynchronized.ref Output.physical_writeln
in
(* Set recipient for PGIP results *)
--- a/src/Pure/Syntax/syntax_trans.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Syntax/syntax_trans.ML Tue Aug 23 15:46:53 2011 -0700
@@ -255,8 +255,19 @@
fun struct_tr structs [Const ("_indexdefault", _)] =
Syntax.free (the_struct structs 1)
| struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
- Syntax.free (the_struct structs
- (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
+ (case Lexicon.read_nat s of
+ SOME n =>
+ let
+ val x = the_struct structs n;
+ val advice =
+ " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
+ (if n = 1 then " (may be omitted)" else "");
+ val _ =
+ legacy_feature
+ ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ s) ^
+ Position.str_of (Position.thread_data ()) ^ advice);
+ in Syntax.free x end
+ | NONE => raise TERM ("struct_tr", [t]))
| struct_tr _ ts = raise TERM ("struct_tr", ts);
--- a/src/Pure/System/isabelle_process.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/System/isabelle_process.ML Tue Aug 23 15:46:53 2011 -0700
@@ -171,7 +171,7 @@
fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
let
val _ = OS.Process.sleep (seconds 0.5); (*yield to raw ML toplevel*)
- val _ = Output.raw_stdout Symbol.STX;
+ val _ = Output.physical_stdout Symbol.STX;
val _ = quick_and_dirty := true;
val _ = Goal.parallel_proofs := 0;
--- a/src/Pure/System/session.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/System/session.ML Tue Aug 23 15:46:53 2011 -0700
@@ -107,7 +107,7 @@
val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
|> Real.fmt (StringCvt.FIX (SOME 2));
val _ =
- Output.raw_stderr ("Timing " ^ item ^ " (" ^
+ Output.physical_stderr ("Timing " ^ item ^ " (" ^
string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
Timing.message timing ^ ", factor " ^ factor ^ ")\n");
in () end
--- a/src/Pure/System/session.scala Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/System/session.scala Tue Aug 23 15:46:53 2011 -0700
@@ -164,10 +164,10 @@
private case class Start(timeout: Time, args: List[String])
private case object Interrupt
- private case class Init_Node(
- name: String, master_dir: String, header: Document.Node_Header, text: String)
- private case class Edit_Node(
- name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
+ private case class Init_Node(name: String, master_dir: String,
+ header: Document.Node_Header, perspective: Text.Perspective, text: String)
+ private case class Edit_Node(name: String, master_dir: String,
+ header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
private case class Change_Node(
name: String,
doc_edits: List[Document.Edit_Command],
@@ -183,7 +183,7 @@
/* incoming edits */
def handle_edits(name: String, master_dir: String,
- header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit]])
+ header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
//{{{
{
val syntax = current_syntax()
@@ -196,7 +196,8 @@
else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
}
def norm_use(s: String): String = file_store.append(master_dir, Path.explode(s))
- val norm_header = Document.Node.norm_header[Text.Edit](norm_import, norm_use, header)
+ val norm_header =
+ Document.Node.norm_header[Text.Edit, Text.Perspective](norm_import, norm_use, header)
val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
@@ -229,22 +230,20 @@
removed <- previous.nodes(name).commands.get_after(prev)
} former_assignment -= removed
- def id_command(command: Command): Document.Command_ID =
+ def id_command(command: Command)
{
if (global_state().lookup_command(command.id).isEmpty) {
global_state.change(_.define_command(command))
prover.get.define_command(command.id, Symbol.encode(command.source))
}
- command.id
}
- val id_edits =
- doc_edits map {
- case (name, edit) =>
- (name, edit.map({ case (c1, c2) => (c1.map(id_command), c2.map(id_command)) }))
- }
+ doc_edits foreach {
+ case (_, edit) =>
+ edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
+ }
global_state.change(_.define_version(version, former_assignment))
- prover.get.edit_version(previous.id, version.id, id_edits)
+ prover.get.edit_version(previous.id, version.id, doc_edits)
}
//}}}
@@ -337,14 +336,18 @@
case Interrupt if prover.isDefined =>
prover.get.interrupt
- case Init_Node(name, master_dir, header, text) if prover.isDefined =>
+ case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
// FIXME compare with existing node
handle_edits(name, master_dir, header,
- List(Document.Node.Clear(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
+ List(Document.Node.Clear(),
+ Document.Node.Edits(List(Text.Edit.insert(0, text))),
+ Document.Node.Perspective(perspective)))
reply(())
- case Edit_Node(name, master_dir, header, text_edits) if prover.isDefined =>
- handle_edits(name, master_dir, header, List(Document.Node.Edits(text_edits)))
+ case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
+ handle_edits(name, master_dir, header,
+ List(Document.Node.Edits(text_edits),
+ Document.Node.Perspective(perspective)))
reply(())
case change: Change_Node if prover.isDefined =>
@@ -372,9 +375,13 @@
def interrupt() { session_actor ! Interrupt }
- def init_node(name: String, master_dir: String, header: Document.Node_Header, text: String)
- { session_actor !? Init_Node(name, master_dir, header, text) }
+ // FIXME simplify signature
+ def init_node(name: String, master_dir: String,
+ header: Document.Node_Header, perspective: Text.Perspective, text: String)
+ { session_actor !? Init_Node(name, master_dir, header, perspective, text) }
- def edit_node(name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
- { session_actor !? Edit_Node(name, master_dir, header, edits) }
+ // FIXME simplify signature
+ def edit_node(name: String, master_dir: String, header: Document.Node_Header,
+ perspective: Text.Perspective, edits: List[Text.Edit])
+ { session_actor !? Edit_Node(name, master_dir, header, perspective, edits) }
}
--- a/src/Pure/Thy/present.ML Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Thy/present.ML Tue Aug 23 15:46:53 2011 -0700
@@ -289,7 +289,8 @@
val documents =
if doc = "" then []
else if not (can File.check_dir document_path) then
- (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); [])
+ (if verbose then Output.physical_stderr "Warning: missing document directory\n"
+ else (); [])
else read_variants doc_variants;
val parent_index_path = Path.append Path.parent index_path;
@@ -403,14 +404,14 @@
File.copy (Path.explode "~~/etc/isabelle.css") html_prefix;
List.app finish_html thys;
List.app (uncurry File.write) files;
- if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
+ if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
else ())
else ();
val _ =
(case dump_prefix of NONE => () | SOME (cp, path) =>
(prepare_sources cp path;
- if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n")
+ if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
else ()));
val doc_paths =
@@ -421,7 +422,8 @@
in isabelle_document true doc_format name tags path html_prefix end);
val _ =
if verbose then
- doc_paths |> List.app (fn doc => Output.raw_stderr ("Document at " ^ show_path doc ^ "\n"))
+ doc_paths
+ |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n"))
else ();
in
browser_info := empty_browser_info;
--- a/src/Pure/Thy/thy_syntax.scala Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Thy/thy_syntax.scala Tue Aug 23 15:46:53 2011 -0700
@@ -97,6 +97,37 @@
+ /** command perspective **/
+
+ def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
+ {
+ if (perspective.isEmpty) Nil
+ else {
+ val result = new mutable.ListBuffer[Command]
+ @tailrec
+ def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
+ {
+ (ranges, commands) match {
+ case (range :: more_ranges, (command, offset) #:: more_commands) =>
+ val command_range = command.range + offset
+ range compare command_range match {
+ case -1 => check_ranges(more_ranges, commands)
+ case 0 =>
+ result += command
+ check_ranges(ranges, more_commands)
+ case 1 => check_ranges(ranges, more_commands)
+ }
+ case _ =>
+ }
+ }
+ val perspective_range = Text.Range(perspective.head.start, perspective.last.stop)
+ check_ranges(perspective, node.command_range(perspective_range).toStream)
+ result.toList
+ }
+ }
+
+
+
/** text edits **/
def text_edits(
@@ -138,7 +169,7 @@
@tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
{
- commands.iterator.find(_.is_unparsed) match {
+ commands.iterator.find(cmd => !cmd.is_defined) match {
case Some(first_unparsed) =>
val first =
commands.reverse_iterator(first_unparsed).
@@ -210,6 +241,14 @@
doc_edits += (name -> Document.Node.Header(header))
nodes += (name -> node.copy(header = header))
}
+
+ case (name, Document.Node.Perspective(text_perspective)) =>
+ val node = nodes(name)
+ val perspective = command_perspective(node, text_perspective)
+ if (!Command.equal_perspective(node.perspective, perspective)) {
+ doc_edits += (name -> Document.Node.Perspective(perspective))
+ nodes += (name -> node.copy(perspective = perspective))
+ }
}
(doc_edits.toList, Document.Version(Document.new_id(), nodes))
}
--- a/src/Tools/jEdit/src/document_model.scala Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Tools/jEdit/src/document_model.scala Tue Aug 23 15:46:53 2011 -0700
@@ -60,10 +60,29 @@
class Document_Model(val session: Session, val buffer: Buffer,
val master_dir: String, val node_name: String, val thy_name: String)
{
- /* pending text edits */
+ /* header */
def node_header(): Exn.Result[Thy_Header] =
+ {
+ Swing_Thread.require()
Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
+ }
+
+
+ /* perspective */
+
+ def perspective(): Text.Perspective =
+ {
+ Swing_Thread.require()
+ Text.perspective(
+ for {
+ doc_view <- Isabelle.document_views(buffer)
+ range <- doc_view.perspective()
+ } yield range)
+ }
+
+
+ /* pending text edits */
private object pending_edits // owned by Swing thread
{
@@ -77,14 +96,15 @@
case Nil =>
case edits =>
pending.clear
- session.edit_node(node_name, master_dir, node_header(), edits)
+ session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
}
}
def init()
{
flush()
- session.init_node(node_name, master_dir, node_header(), Isabelle.buffer_text(buffer))
+ session.init_node(node_name, master_dir,
+ node_header(), perspective(), Isabelle.buffer_text(buffer))
}
private val delay_flush =
--- a/src/Tools/jEdit/src/document_view.scala Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Tools/jEdit/src/document_view.scala Tue Aug 23 15:46:53 2011 -0700
@@ -10,6 +10,7 @@
import isabelle._
+import scala.collection.mutable
import scala.actors.Actor._
import java.lang.System
@@ -86,7 +87,7 @@
}
- /* visible line ranges */
+ /* visible text range */
// simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
// NB: jEdit already normalizes \r\n and \r to \n
@@ -96,14 +97,14 @@
Text.Range(start, stop)
}
- def screen_lines_range(): Text.Range =
+ def visible_range(): Text.Range =
{
val start = text_area.getScreenLineStartOffset(0)
val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
}
- def invalidate_line_range(range: Text.Range)
+ def invalidate_range(range: Text.Range)
{
text_area.invalidateLineRange(
model.buffer.getLineOfOffset(range.start),
@@ -111,6 +112,22 @@
}
+ /* perspective */
+
+ def perspective(): Text.Perspective =
+ {
+ Swing_Thread.require()
+ Text.perspective(
+ for {
+ i <- 0 until text_area.getVisibleLines
+ val start = text_area.getScreenLineStartOffset(i)
+ val stop = text_area.getScreenLineEndOffset(i)
+ if start >= 0 && stop >= 0
+ }
+ yield Text.Range(start, stop))
+ }
+
+
/* snapshot */
// owned by Swing thread
@@ -224,9 +241,9 @@
if (control) init_popup(snapshot, x, y)
- _highlight_range map { case (range, _) => invalidate_line_range(range) }
+ _highlight_range map { case (range, _) => invalidate_range(range) }
_highlight_range = if (control) subexp_range(snapshot, x, y) else None
- _highlight_range map { case (range, _) => invalidate_line_range(range) }
+ _highlight_range map { case (range, _) => invalidate_range(range) }
}
}
}
@@ -415,15 +432,15 @@
val buffer = model.buffer
Isabelle.swing_buffer_lock(buffer) {
val (updated, snapshot) = flush_snapshot()
- val visible_range = screen_lines_range()
+ val visible = visible_range()
if (updated || changed.exists(snapshot.node.commands.contains))
overview.repaint()
- if (updated) invalidate_line_range(visible_range)
+ if (updated) invalidate_range(visible)
else {
val visible_cmds =
- snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+ snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
if (visible_cmds.exists(changed)) {
for {
line <- 0 until text_area.getVisibleLines
--- a/src/Tools/jEdit/src/plugin.scala Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 23 15:46:53 2011 -0700
@@ -199,6 +199,13 @@
def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
+ def document_views(buffer: Buffer): List[Document_View] =
+ for {
+ text_area <- jedit_text_areas(buffer).toList
+ val doc_view = document_view(text_area)
+ if doc_view.isDefined
+ } yield doc_view.get
+
def init_model(buffer: Buffer)
{
swing_buffer_lock(buffer) {