--- a/src/HOL/Groups.thy Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Groups.thy Wed Aug 24 09:08:07 2011 -0700
@@ -103,11 +103,6 @@
hide_const (open) zero one
-syntax
- "_index1" :: index ("\<^sub>1")
-translations
- (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
-
lemma Let_0 [simp]: "Let 0 f = f 0"
unfolding Let_def ..
--- a/src/HOL/Library/Quotient_Set.thy Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Library/Quotient_Set.thy Wed Aug 24 09:08:07 2011 -0700
@@ -33,7 +33,7 @@
lemma collect_rsp[quot_respect]:
assumes "Quotient R Abs Rep"
shows "((R ===> op =) ===> set_rel R) Collect Collect"
- by (auto intro!: fun_relI simp add: fun_rel_def set_rel_def)
+ by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
lemma collect_prs[quot_preserve]:
assumes "Quotient R Abs Rep"
@@ -44,7 +44,7 @@
lemma union_rsp[quot_respect]:
assumes "Quotient R Abs Rep"
shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
- by (intro fun_relI) (auto simp add: set_rel_def)
+ by (intro fun_relI) (simp add: set_rel_def)
lemma union_prs[quot_preserve]:
assumes "Quotient R Abs Rep"
@@ -55,7 +55,7 @@
lemma diff_rsp[quot_respect]:
assumes "Quotient R Abs Rep"
shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
- by (intro fun_relI) (auto simp add: set_rel_def)
+ by (intro fun_relI) (simp add: set_rel_def)
lemma diff_prs[quot_preserve]:
assumes "Quotient R Abs Rep"
@@ -74,4 +74,13 @@
unfolding fun_eq_iff
by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
+lemma mem_prs[quot_preserve]:
+ assumes "Quotient R Abs Rep"
+ shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
+ by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
+
+lemma mem_rsp[quot_respect]:
+ shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
+ by (intro fun_relI) (simp add: set_rel_def)
+
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 24 09:08:07 2011 -0700
@@ -550,44 +550,53 @@
end
-val e_override_params =
+fun e_override_params timeout =
[("provers", "e"),
("max_relevant", "0"),
("type_enc", "poly_guards?"),
("sound", "true"),
- ("slicing", "false")]
+ ("slicing", "false"),
+ ("timeout", timeout |> Time.toSeconds |> string_of_int)]
-val vampire_override_params =
+fun vampire_override_params timeout =
[("provers", "vampire"),
("max_relevant", "0"),
("type_enc", "poly_tags"),
("sound", "true"),
- ("slicing", "false")]
+ ("slicing", "false"),
+ ("timeout", timeout |> Time.toSeconds |> string_of_int)]
fun run_reconstructor trivial full m name reconstructor named_thms id
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
let
- fun do_reconstructor thms ctxt =
- (if !reconstructor = "sledgehammer_tac" then
- (fn ctxt => fn thms =>
- Method.insert_tac thms THEN'
- (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
- K (K (K all_tac))) ctxt thms
- fun apply_reconstructor thms =
- Mirabelle.can_apply timeout (do_reconstructor thms) st
+ fun do_reconstructor named_thms ctxt =
+ let
+ val ref_of_str =
+ suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
+ #> fst
+ val thms = named_thms |> maps snd
+ val facts = named_thms |> map (ref_of_str o fst o fst)
+ val relevance_override = {add = facts, del = [], only = true}
+ in
+ if !reconstructor = "sledgehammer_tac" then
+ Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+ (e_override_params timeout) relevance_override
+ ORELSE'
+ Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+ (vampire_override_params timeout) relevance_override
+ else if !reconstructor = "smt" then
+ SMT_Solver.smt_tac ctxt thms
+ else if full orelse !reconstructor = "metis (full_types)" then
+ Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] ctxt thms
+ else if !reconstructor = "metis (no_types)" then
+ Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] ctxt thms
+ else if !reconstructor = "metis" then
+ Metis_Tactics.metis_tac [] ctxt thms
+ else
+ K all_tac
+ end
+ fun apply_reconstructor named_thms =
+ Mirabelle.can_apply timeout (do_reconstructor named_thms) st
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
| with_time (true, t) = (change_data id (inc_reconstructor_success m);
@@ -599,8 +608,8 @@
if name = "proof" then change_data id (inc_reconstructor_proofs m)
else ();
"succeeded (" ^ string_of_int t ^ ")")
- fun timed_reconstructor thms =
- (with_time (Mirabelle.cpu_time apply_reconstructor thms), true)
+ fun timed_reconstructor named_thms =
+ (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true)
handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m);
("timeout", false))
| ERROR msg => ("error: " ^ msg, false)
@@ -610,7 +619,7 @@
val _ = if trivial then ()
else change_data id (inc_reconstructor_nontriv_calls m)
in
- maps snd named_thms
+ named_thms
|> timed_reconstructor
|>> log o prefix (reconstructor_tag reconstructor id)
|> snd
--- a/src/HOL/TPTP/CASC_Setup.thy Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/TPTP/CASC_Setup.thy Wed Aug 24 09:08:07 2011 -0700
@@ -119,14 +119,16 @@
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 []
+ Sledgehammer_Filter.no_relevance_override))
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 []
+ Sledgehammer_Filter.no_relevance_override))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "metis"
(ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 24 09:08:07 2011 -0700
@@ -1059,16 +1059,13 @@
| formula => SOME formula
end
-fun make_conjecture ctxt format type_enc ps =
- let
- val thy = Proof_Context.theory_of ctxt
- val last = length ps - 1
- in
- map2 (fn j => fn ((name, loc), (kind, t)) =>
- t |> make_formula thy type_enc (format <> CNF) name loc kind
- |> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot)
- (0 upto last) ps
- end
+fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+ | s_not_trueprop t = s_not t
+
+fun make_conjecture thy format type_enc =
+ map (fn ((name, loc), (kind, t)) =>
+ t |> kind = Conjecture ? s_not_trueprop
+ |> make_formula thy type_enc (format <> CNF) name loc kind)
(** Finite and infinite type inference **)
@@ -1552,7 +1549,7 @@
|> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
val facts = facts |> map (apsnd (pair Axiom))
val conjs =
- map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
+ map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
|> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
val ((conjs, facts), lambdas) =
if preproc then
@@ -1563,7 +1560,7 @@
|>> apfst (map (apsnd (apsnd freeze_term)))
else
((conjs, facts), [])
- val conjs = conjs |> make_conjecture ctxt format type_enc
+ val conjs = conjs |> make_conjecture thy format type_enc
val (fact_names, facts) =
facts
|> map_filter (fn (name, (_, t)) =>
--- a/src/HOL/Tools/ATP/atp_util.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_util.ML Wed Aug 24 09:08:07 2011 -0700
@@ -272,7 +272,7 @@
(* Converts an elim-rule into an equivalent theorem that does not have the
predicate variable. Leaves other theorems unchanged. We simply instantiate
- the conclusion variable to False. (Cf. "transform_elim_theorem" in
+ the conclusion variable to "False". (Cf. "transform_elim_theorem" in
"Meson_Clausify".) *)
fun transform_elim_prop t =
case Logic.strip_imp_concl t of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Aug 24 09:08:07 2011 -0700
@@ -38,6 +38,7 @@
val trace : bool Config.T
val ignore_no_atp : bool Config.T
val instantiate_inducts : bool Config.T
+ val no_relevance_override : relevance_override
val const_names_in_fact :
theory -> (string * typ -> term list -> bool * term list) -> term
-> string list
@@ -100,6 +101,8 @@
del : (Facts.ref * Attrib.src list) list,
only : bool}
+val no_relevance_override = {add = [], del = [], only = false}
+
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
val abs_name = sledgehammer_prefix ^ "abs"
val skolem_prefix = sledgehammer_prefix ^ "sko"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 24 09:08:07 2011 -0700
@@ -22,6 +22,7 @@
open ATP_Systems
open ATP_Translate
open Sledgehammer_Util
+open Sledgehammer_Filter
open Sledgehammer_Provers
open Sledgehammer_Minimize
open Sledgehammer_Run
@@ -46,7 +47,6 @@
(** Sledgehammer commands **)
-val no_relevance_override = {add = [], del = [], only = false}
fun add_relevance_override ns : relevance_override =
{add = ns, del = [], only = false}
fun del_relevance_override ns : relevance_override =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Aug 24 09:08:07 2011 -0700
@@ -57,16 +57,16 @@
(if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
else "") ^ "...")
val {goal, ...} = Proof.goal state
+ val facts =
+ facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_enc = type_enc, sound = true,
- relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
+ relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slicing = false,
timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
- val facts =
- facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts, smt_filter = NONE}
--- a/src/HOL/ex/sledgehammer_tactics.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/HOL/ex/sledgehammer_tactics.ML Wed Aug 24 09:08:07 2011 -0700
@@ -7,16 +7,22 @@
signature SLEDGEHAMMER_TACTICS =
sig
+ type relevance_override = Sledgehammer_Filter.relevance_override
+
val sledgehammer_with_metis_tac :
- Proof.context -> (string * string) list -> int -> tactic
+ Proof.context -> (string * string) list -> relevance_override -> int
+ -> tactic
val sledgehammer_as_oracle_tac :
- Proof.context -> (string * string) list -> int -> tactic
+ Proof.context -> (string * string) list -> relevance_override -> int
+ -> tactic
end;
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
struct
-fun run_atp override_params i n ctxt goal =
+open Sledgehammer_Filter
+
+fun run_atp override_params relevance_override i n ctxt goal =
let
val chained_ths = [] (* a tactic has no chained ths *)
val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
@@ -30,7 +36,6 @@
Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
val relevance_fudge =
Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
- val relevance_override = {add = [], del = [], only = false}
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
val facts =
Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
@@ -62,16 +67,17 @@
|> Source.exhaust
end
-fun sledgehammer_with_metis_tac ctxt override_params i th =
- case run_atp override_params i i ctxt th of
+fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
+ case run_atp override_params relevance_override i i ctxt th of
SOME facts =>
Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
| NONE => Seq.empty
-fun sledgehammer_as_oracle_tac ctxt override_params i th =
+fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
let
val thy = Proof_Context.theory_of ctxt
- val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th
+ val xs = run_atp (override_params @ [("sound", "true")]) relevance_override
+ i i ctxt th
in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
end;
--- a/src/Pure/General/timing.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/General/timing.ML Wed Aug 24 09:08:07 2011 -0700
@@ -20,6 +20,7 @@
val start: unit -> start
val result: start -> timing
val timing: ('a -> 'b) -> 'a -> timing * 'b
+ val is_relevant: timing -> bool
val message: timing -> string
end
@@ -67,11 +68,6 @@
(* timing messages *)
-fun message {elapsed, cpu, gc} =
- Time.toString elapsed ^ "s elapsed time, " ^
- Time.toString cpu ^ "s cpu time, " ^
- Time.toString gc ^ "s GC time" handle Time.Time => "";
-
val min_time = Time.fromMilliseconds 1;
fun is_relevant {elapsed, cpu, gc} =
@@ -79,6 +75,11 @@
Time.>= (cpu, min_time) orelse
Time.>= (gc, min_time);
+fun message {elapsed, cpu, gc} =
+ Time.toString elapsed ^ "s elapsed time, " ^
+ Time.toString cpu ^ "s cpu time, " ^
+ Time.toString gc ^ "s GC time" handle Time.Time => "";
+
fun cond_timeit enabled msg e =
if enabled then
let
--- a/src/Pure/PIDE/document.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/PIDE/document.ML Wed Aug 24 09:08:07 2011 -0700
@@ -24,9 +24,10 @@
type edit = string * node_edit
type state
val init_state: state
+ val define_command: command_id -> string -> state -> state
val join_commands: state -> unit
val cancel_execution: state -> Future.task list
- val define_command: command_id -> string -> state -> state
+ val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
val execute: version_id -> state -> state
val state: unit -> state
@@ -61,50 +62,62 @@
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
abstype node = Node of
- {header: node_header,
+ {touched: bool,
+ 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, perspective, entries, result) =
- Node {header = header, perspective = perspective, entries = entries, result = result};
+fun make_node (touched, header, perspective, entries, result) =
+ Node {touched = touched, 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 {touched, header, perspective, entries, result}) =
+ make_node (f (touched, header, perspective, entries, result));
-val no_perspective: perspective = (K false, []);
+fun make_perspective ids : perspective =
+ (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids);
+
+val no_perspective = make_perspective [];
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);
+ make_node (false, 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));
+ map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result));
(* basic components *)
+fun is_touched (Node {touched, ...}) = touched;
+fun set_touched touched =
+ map_node (fn (_, header, perspective, entries, result) =>
+ (touched, header, perspective, entries, result));
+
fun get_header (Node {header, ...}) = header;
fun set_header header =
- map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
+ map_node (fn (touched, _, perspective, entries, result) =>
+ (touched, header, perspective, 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 set_perspective ids =
+ map_node (fn (touched, header, _, entries, result) =>
+ (touched, header, make_perspective ids, entries, result));
-fun map_entries f (Node {header, perspective, entries, result}) =
- make_node (header, perspective, f entries, result);
+fun map_entries f =
+ map_node (fn (touched, header, perspective, entries, result) =>
+ (touched, 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.force result);
fun set_result result =
- map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
+ map_node (fn (touched, header, perspective, entries, _) =>
+ (touched, 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);
@@ -146,35 +159,47 @@
fun nodes_of (Version nodes) = nodes;
val node_of = get_node o nodes_of;
+local
+
fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
-fun touch_descendants name nodes =
- fold (fn desc => desc <> name ? update_node desc (map_entries (reset_after NONE)))
+fun touch_node name nodes =
+ fold (fn desc =>
+ update_node desc (set_touched true) #>
+ desc <> name ? update_node desc (map_entries (reset_after NONE)))
(Graph.all_succs nodes [name]) nodes;
+in
+
fun edit_nodes (name, node_edit) (Version nodes) =
Version
- (touch_descendants name
- (case node_edit of
- Clear => update_node name clear_node nodes
- | Edits edits =>
- nodes
- |> update_node name (edit_node edits)
- | Header header =>
- let
- val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
- val nodes1 = nodes
- |> default_node name
- |> fold default_node parents;
- val nodes2 = nodes1
- |> Graph.Keys.fold
- (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
- 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
- | Perspective perspective =>
- update_node name (set_perspective perspective) nodes));
+ (case node_edit of
+ Clear =>
+ nodes
+ |> update_node name clear_node
+ |> touch_node name
+ | Edits edits =>
+ nodes
+ |> update_node name (edit_node edits)
+ |> touch_node name
+ | Header header =>
+ let
+ val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
+ val nodes1 = nodes
+ |> default_node name
+ |> fold default_node parents;
+ val nodes2 = nodes1
+ |> Graph.Keys.fold
+ (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
+ 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
+ |> touch_node name
+ | Perspective perspective =>
+ update_node name (set_perspective perspective) nodes);
+
+end;
fun put_node (name, node) (Version nodes) =
Version (update_node name (K node) nodes);
@@ -270,7 +295,8 @@
local
-fun timing tr t = Toplevel.status tr (Markup.timing t);
+fun timing tr t =
+ if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
fun proof_status tr st =
(case try Toplevel.proof_of st of
@@ -320,6 +346,16 @@
(** editing **)
+(* perspective *)
+
+fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state =
+ let
+ val old_version = the_version state old_id;
+ val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *)
+ val new_version = edit_nodes (name, Perspective perspective) old_version;
+ in define_version new_id new_version state end;
+
+
(* edit *)
local
@@ -329,11 +365,32 @@
NONE => true
| SOME exec' => exec' <> exec);
-fun new_exec (command_id, command) (assigns, execs, exec) =
+fun init_theory deps name node =
let
+ val (thy_name, imports, uses) = Exn.release (get_header node);
+ (* FIXME provide files via Scala layer *)
+ val (dir, files) =
+ if ML_System.platform_is_cygwin then (Path.current, [])
+ else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
+
+ val parents =
+ imports |> map (fn import =>
+ (case Thy_Info.lookup_theory import of (* FIXME more robust!? *)
+ SOME thy => thy
+ | 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;
+
+fun new_exec state init command_id (assigns, execs, exec) =
+ let
+ val command = the_command state command_id;
val exec_id' = new_id ();
val exec' = exec |> Lazy.map (fn (st, _) =>
- let val tr = Toplevel.put_id (print_id exec_id') (Future.join command)
+ let val tr =
+ Future.join command
+ |> Toplevel.modify_init init
+ |> Toplevel.put_id (print_id exec_id');
in run_command tr st end);
in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end;
@@ -348,46 +405,32 @@
val updates =
nodes_of new_version |> Graph.schedule
(fn deps => fn (name, node) =>
- (case first_entry NONE (is_changed (node_of old_version name)) node of
- NONE => Future.value (([], [], []), node)
- | SOME ((prev, id), _) =>
- let
- fun init () =
- let
- val (thy_name, imports, uses) = Exn.release (get_header node);
- (* FIXME provide files via Scala layer *)
- val (dir, files) =
- if ML_System.platform_is_cygwin then (Path.current, [])
- else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
-
- val parents =
- imports |> map (fn import =>
- (case Thy_Info.lookup_theory import of
- SOME thy => thy
- | 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;
- fun get_command id =
- (id, the_command state id |> Future.map (Toplevel.modify_init init));
- in
- (singleton o Future.forks)
- {name = "Document.edit", group = NONE,
- deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
- (fn () =>
- let
- val prev_exec =
- (case prev of
- NONE => no_id
- | SOME prev_id => the_default no_id (the_entry node prev_id));
- val (assigns, execs, last_exec) =
- fold_entries (SOME id) (new_exec o get_command o #2 o #1)
- node ([], [], #2 (the_exec state prev_exec));
- val node' = node
- |> fold update_entry assigns
- |> set_result (Lazy.map #1 last_exec);
- in ((assigns, execs, [(name, node')]), node') end)
- end))
+ if not (is_touched node) then Future.value (([], [], []), node)
+ else
+ (case first_entry NONE (is_changed (node_of old_version name)) node of
+ NONE => Future.value (([], [], []), set_touched false node)
+ | SOME ((prev, id), _) =>
+ let
+ fun init () = init_theory deps name node;
+ in
+ (singleton o Future.forks)
+ {name = "Document.edit", group = NONE,
+ deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
+ (fn () =>
+ let
+ val prev_exec =
+ (case prev of
+ NONE => no_id
+ | SOME prev_id => the_default no_id (the_entry node prev_id));
+ val (assigns, execs, last_exec) =
+ fold_entries (SOME id) (new_exec state init o #2 o #1)
+ node ([], [], #2 (the_exec state prev_exec));
+ val node' = node
+ |> fold update_entry assigns
+ |> set_result (Lazy.map #1 last_exec)
+ |> set_touched false;
+ in ((assigns, execs, [(name, node')]), node') end)
+ end))
|> Future.joins |> map #1;
val state' = state
@@ -411,9 +454,8 @@
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 *)
+ if #1 (get_perspective node) command_id
then ignore (Lazy.future Future.default_params print)
else ();
in () end;
--- a/src/Pure/PIDE/document.scala Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/PIDE/document.scala Wed Aug 24 09:08:07 2011 -0700
@@ -54,11 +54,10 @@
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, B](f: String => String, g: String => String, header: Node_Header)
- : Header[A, B] =
+ def norm_header(f: String => String, g: String => String, header: Node_Header): Node_Header =
header match {
- case Exn.Res(h) => Header[A, B](Exn.capture { h.norm_deps(f, g) })
- case exn => Header[A, B](exn)
+ case Exn.Res(h) => Exn.capture { h.norm_deps(f, g) }
+ case exn => exn
}
val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
@@ -83,6 +82,9 @@
val blobs: Map[String, Blob],
val commands: Linear_Set[Command])
{
+ def clear: Node = Node.empty.copy(header = header)
+
+
/* commands */
private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
@@ -146,7 +148,8 @@
val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
}
- sealed case class Version(val id: Version_ID, val nodes: Map[String, Node])
+ type Nodes = Map[String, Node]
+ sealed case class Version(val id: Version_ID, val nodes: Nodes)
/* changes of plain text, eventually resulting in document edits */
@@ -221,8 +224,8 @@
sealed case class State(
val versions: Map[Version_ID, Version] = Map(),
- val commands: Map[Command_ID, Command.State] = Map(),
- val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
+ val commands: Map[Command_ID, Command.State] = Map(), // static markup from define_command
+ val execs: Map[Exec_ID, Command.State] = Map(), // dynamic markup from execution
val assignments: Map[Version_ID, State.Assignment] = Map(),
val disposed: Set[ID] = Set(), // FIXME unused!?
val history: History = History.init)
@@ -248,15 +251,15 @@
def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
- def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
+ def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
def the_assignment(version: Version): State.Assignment =
assignments.getOrElse(version.id, fail)
def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
execs.get(id) match {
- case Some((st, occs)) =>
+ case Some(st) =>
val new_st = st.accumulate(message)
- (new_st, copy(execs = execs + (id -> (new_st, occs))))
+ (new_st, copy(execs = execs + (id -> new_st)))
case None =>
commands.get(id) match {
case Some(st) =>
@@ -269,14 +272,13 @@
def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
{
val version = the_version(id)
- val occs = Set(version) // FIXME unused (!?)
var new_execs = execs
val assigned_execs =
for ((cmd_id, exec_id) <- edits) yield {
val st = the_command(cmd_id)
if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
- new_execs += (exec_id -> (st, occs))
+ new_execs += (exec_id -> st)
(st.command, exec_id)
}
val new_assignment = the_assignment(version).assign(assigned_execs)
@@ -290,7 +292,14 @@
case None => false
}
- def extend_history(previous: Future[Version],
+ def is_stable(change: Change): Boolean =
+ change.is_finished && is_assigned(change.version.get_finished)
+
+ def tip_stable: Boolean = is_stable(history.tip)
+ def recent_stable: Option[Change] = history.undo_list.find(is_stable)
+
+ def continue_history(
+ previous: Future[Version],
edits: List[Edit_Text],
version: Future[Version]): (Change, State) =
{
@@ -302,11 +311,8 @@
// persistent user-view
def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
{
- val found_stable = history.undo_list.find(change =>
- change.is_finished && is_assigned(change.version.get_finished))
- require(found_stable.isDefined)
- val stable = found_stable.get
- val latest = history.undo_list.head
+ val stable = recent_stable.get
+ val latest = history.tip
// FIXME proper treatment of removed nodes
val edits =
@@ -323,7 +329,7 @@
def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
def state(command: Command): Command.State =
- try { the_exec_state(the_assignment(version).get_finished.getOrElse(command, fail)) }
+ try { the_exec(the_assignment(version).get_finished.getOrElse(command, fail)) }
catch { case _: State.Fail => command.empty_state }
def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
--- a/src/Pure/PIDE/isar_document.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/PIDE/isar_document.ML Wed Aug 24 09:08:07 2011 -0700
@@ -12,6 +12,22 @@
(fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
val _ =
+ Isabelle_Process.add_command "Isar_Document.update_perspective"
+ (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
+ let
+ val old_id = Document.parse_id old_id_string;
+ val new_id = Document.parse_id new_id_string;
+ val ids = YXML.parse_body ids_yxml
+ |> let open XML.Decode in list int end;
+
+ val _ = Future.join_tasks (Document.cancel_execution state);
+ in
+ state
+ |> Document.update_perspective old_id new_id name ids
+ |> Document.execute new_id
+ end));
+
+val _ =
Isabelle_Process.add_command "Isar_Document.edit_version"
(fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
let
@@ -31,15 +47,15 @@
fn (a, []) => Document.Perspective (map int_atom a)]))
end;
- val running = Document.cancel_execution state;
- val (updates, state') = Document.edit old_id new_id edits state;
- val _ = Future.join_tasks running;
- val _ = Document.join_commands state';
- val _ =
- Output.status (Markup.markup (Markup.assign new_id)
- (implode (map (Markup.markup_only o Markup.edit) updates)));
- val state'' = Document.execute new_id state';
- in state'' end));
+ val running = Document.cancel_execution state;
+ val (updates, state') = Document.edit old_id new_id edits state;
+ val _ = Future.join_tasks running;
+ val _ = Document.join_commands state';
+ val _ =
+ Output.status (Markup.markup (Markup.assign new_id)
+ (implode (map (Markup.markup_only o Markup.edit) updates)));
+ val state'' = Document.execute new_id state';
+ in state'' end));
val _ =
Isabelle_Process.add_command "Isar_Document.invoke_scala"
--- a/src/Pure/PIDE/isar_document.scala Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/PIDE/isar_document.scala Wed Aug 24 09:08:07 2011 -0700
@@ -139,6 +139,17 @@
/* document versions */
+ def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
+ name: String, perspective: Command.Perspective)
+ {
+ val ids =
+ { import XML.Encode._
+ list(long)(perspective.map(_.id)) }
+
+ input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name,
+ YXML.string_of_body(ids))
+ }
+
def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
edits: List[Document.Edit_Command])
{
--- a/src/Pure/Syntax/syntax_trans.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/Syntax/syntax_trans.ML Wed Aug 24 09:08:07 2011 -0700
@@ -252,21 +252,22 @@
if 1 <= i andalso i <= length structs then nth structs (i - 1)
else error ("Illegal reference to implicit structure #" ^ string_of_int i);
-fun struct_tr structs [Const ("_indexdefault", _)] =
- Syntax.free (the_struct structs 1)
+fun legacy_struct structs i =
+ let
+ val x = the_struct structs i;
+ val _ =
+ legacy_feature
+ ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ string_of_int i) ^
+ Position.str_of (Position.thread_data ()) ^
+ " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
+ (if i = 1 then " (may be omitted)" else ""))
+ in x end;
+
+fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs 1)
+ | struct_tr structs [Const ("_index1", _)] = Syntax.free (legacy_struct structs 1)
| struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
(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
+ SOME i => Syntax.free (legacy_struct structs i)
| NONE => raise TERM ("struct_tr", [t]))
| struct_tr _ ts = raise TERM ("struct_tr", ts);
--- a/src/Pure/System/session.scala Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/System/session.scala Wed Aug 24 09:08:07 2011 -0700
@@ -159,6 +159,28 @@
val thy_info = new Thy_Info(thy_load)
+ def header_edit(name: String, master_dir: String,
+ header: Document.Node_Header): Document.Edit_Text =
+ {
+ def norm_import(s: String): String =
+ {
+ val thy_name = Thy_Header.base_name(s)
+ if (thy_load.is_loaded(thy_name)) thy_name
+ 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 header1: Document.Node_Header =
+ header match {
+ case Exn.Res(Thy_Header(thy_name, _, _))
+ if (thy_load.is_loaded(thy_name)) =>
+ Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
+ case _ => Document.Node.norm_header(norm_import, norm_use, header)
+ }
+ (name, Document.Node.Header(header1))
+ }
+
/* actor messages */
@@ -180,6 +202,27 @@
var prover: Option[Isabelle_Process with Isar_Document] = None
+ /* perspective */
+
+ def update_perspective(name: String, text_perspective: Text.Perspective)
+ {
+ val previous = global_state().history.tip.version.get_finished
+ val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
+
+ val text_edits: List[Document.Edit_Text] =
+ List((name, Document.Node.Perspective(text_perspective)))
+ val change =
+ global_state.change_yield(
+ _.continue_history(Future.value(previous), text_edits, Future.value(version)))
+
+ val assignment = global_state().the_assignment(previous).get_finished
+ global_state.change(_.define_version(version, assignment))
+ global_state.change_yield(_.assign(version.id, Nil))
+
+ prover.get.update_perspective(previous.id, version.id, name, perspective)
+ }
+
+
/* incoming edits */
def handle_edits(name: String, master_dir: String,
@@ -189,20 +232,10 @@
val syntax = current_syntax()
val previous = global_state().history.tip.version
- def norm_import(s: String): String =
- {
- val name = Thy_Header.base_name(s)
- if (thy_load.is_loaded(name)) name
- 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, Text.Perspective](norm_import, norm_use, header)
-
- val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
+ val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit))
val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
val change =
- global_state.change_yield(_.extend_history(previous, text_edits, result.map(_._2)))
+ global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
result.map {
case (doc_edits, _) =>
@@ -213,6 +246,18 @@
//}}}
+ /* exec state assignment */
+
+ def handle_assign(id: Document.Version_ID, edits: List[(Document.Command_ID, Document.Exec_ID)])
+ //{{{
+ {
+ val cmds = global_state.change_yield(_.assign(id, edits))
+ for (cmd <- cmds) command_change_buffer ! cmd
+ assignments.event(Session.Assignment)
+ }
+ //}}}
+
+
/* resulting changes */
def handle_change(change: Change_Node)
@@ -292,11 +337,7 @@
else if (result.is_status) {
result.body match {
case List(Isar_Document.Assign(id, edits)) =>
- try {
- val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
- for (cmd <- cmds) command_change_buffer ! cmd
- assignments.event(Session.Assignment)
- }
+ try { handle_assign(id, edits) }
catch { case _: Document.State.Fail => bad_result(result) }
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
case List(Keyword.Keyword_Decl(name)) => syntax += name
@@ -345,9 +386,11 @@
reply(())
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)))
+ if (text_edits.isEmpty && global_state().tip_stable)
+ update_perspective(name, perspective)
+ else
+ handle_edits(name, master_dir, header,
+ List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
reply(())
case change: Change_Node if prover.isDefined =>
--- a/src/Pure/Thy/thy_syntax.scala Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/Thy/thy_syntax.scala Wed Aug 24 09:08:07 2011 -0700
@@ -97,7 +97,7 @@
- /** command perspective **/
+ /** perspective **/
def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
{
@@ -126,6 +126,26 @@
}
}
+ def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective)
+ : (Command.Perspective, Option[Document.Nodes]) =
+ {
+ val node = nodes(name)
+ val perspective = command_perspective(node, text_perspective)
+ val new_nodes =
+ if (Command.equal_perspective(node.perspective, perspective)) None
+ else Some(nodes + (name -> node.copy(perspective = perspective)))
+ (perspective, new_nodes)
+ }
+
+ def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective)
+ : (Command.Perspective, Document.Version) =
+ {
+ val nodes = previous.nodes
+ val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
+ val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes)
+ (perspective, version)
+ }
+
/** text edits **/
@@ -212,7 +232,7 @@
edits foreach {
case (name, Document.Node.Clear()) =>
doc_edits += (name -> Document.Node.Clear())
- nodes -= name
+ nodes += (name -> nodes(name).clear)
case (name, Document.Node.Edits(text_edits)) =>
val node = nodes(name)
@@ -243,11 +263,11 @@
}
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))
+ update_perspective(nodes, name, text_perspective) match {
+ case (_, None) =>
+ case (perspective, Some(nodes1)) =>
+ doc_edits += (name -> Document.Node.Perspective(perspective))
+ nodes = nodes1
}
}
(doc_edits.toList, Document.Version(Document.new_id(), nodes))
--- a/src/Pure/pure_thy.ML Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Pure/pure_thy.ML Wed Aug 24 09:08:07 2011 -0700
@@ -127,6 +127,7 @@
("_strip_positions", typ "'a", NoSyn),
("_constify", typ "num => num_const", Delimfix "_"),
("_constify", typ "float_token => float_const", Delimfix "_"),
+ ("_index1", typ "index", Delimfix "\\<^sub>1"),
("_indexnum", typ "num_const => index", Delimfix "\\<^sub>_"),
("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"),
("_indexdefault", typ "index", Delimfix ""),
--- a/src/Tools/jEdit/src/document_model.scala Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Tools/jEdit/src/document_model.scala Wed Aug 24 09:08:07 2011 -0700
@@ -87,16 +87,25 @@
private object pending_edits // owned by Swing thread
{
private val pending = new mutable.ListBuffer[Text.Edit]
+ private var pending_perspective = false
+ private var last_perspective: Text.Perspective = Nil
+
def snapshot(): List[Text.Edit] = pending.toList
def flush()
{
Swing_Thread.require()
+
+ val new_perspective =
+ if (pending_perspective) { pending_perspective = false; perspective() }
+ else last_perspective
+
snapshot() match {
- case Nil =>
+ case Nil if new_perspective == last_perspective =>
case edits =>
pending.clear
- session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
+ last_perspective = new_perspective
+ session.edit_node(node_name, master_dir, node_header(), new_perspective, edits)
}
}
@@ -116,6 +125,18 @@
pending += edit
delay_flush()
}
+
+ def update_perspective()
+ {
+ pending_perspective = true
+ delay_flush()
+ }
+ }
+
+ def update_perspective()
+ {
+ Swing_Thread.require()
+ pending_edits.update_perspective()
}
--- a/src/Tools/jEdit/src/document_view.scala Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Tools/jEdit/src/document_view.scala Wed Aug 24 09:08:07 2011 -0700
@@ -25,7 +25,8 @@
import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
import org.gjt.sp.jedit.gui.RolloverButton
import org.gjt.sp.jedit.options.GutterOptionPane
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter,
+ ScrollListener}
import org.gjt.sp.jedit.syntax.{SyntaxStyle}
@@ -127,6 +128,16 @@
yield Text.Range(start, stop))
}
+ private def update_perspective = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ {
+ model.update_perspective()
+ }
+ }
+
/* snapshot */
@@ -467,6 +478,7 @@
private def activate()
{
val painter = text_area.getPainter
+ painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
text_area_painter.activate()
text_area.getGutter.addExtension(gutter_painter)
@@ -492,6 +504,7 @@
text_area.getGutter.removeExtension(gutter_painter)
text_area_painter.deactivate()
painter.removeExtension(tooltip_painter)
+ painter.removeExtension(update_perspective)
exit_popup()
}
}
--- a/src/Tools/jEdit/src/plugin.scala Wed Aug 24 09:08:00 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala Wed Aug 24 09:08:07 2011 -0700
@@ -409,7 +409,7 @@
Isabelle.start_session()
case msg: BufferUpdate
- if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+ if msg.getWhat == BufferUpdate.LOADED =>
val buffer = msg.getBuffer
if (buffer != null && Isabelle.session.is_ready)