--- a/src/HOL/ATP.thy Wed Jul 06 13:52:42 2011 +0200
+++ b/src/HOL/ATP.thy Wed Jul 06 13:57:52 2011 +0200
@@ -39,6 +39,11 @@
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
"fequal x y \<longleftrightarrow> (x = y)"
+definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
+"fAll P \<longleftrightarrow> All P"
+
+definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
+"fEx P \<longleftrightarrow> Ex P"
subsection {* Setup *}
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Jul 06 13:52:42 2011 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Jul 06 13:57:52 2011 +0200
@@ -844,7 +844,7 @@
by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
qed
-lemma sigma_sets_subseteq: "A \<subseteq> sigma_sets X A"
+lemma sigma_sets_superset_generator: "A \<subseteq> sigma_sets X A"
by (auto intro: sigma_sets.Basic)
lemma (in product_prob_space) infprod_algebra_alt:
@@ -859,7 +859,7 @@
fix J assume J: "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}"
have "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> emb I J ` sets (Pi\<^isub>M J M)" by auto
also have "\<dots> \<subseteq> ?G" using J by (rule UN_upper)
- also have "\<dots> \<subseteq> sigma_sets ?O ?G" by (rule sigma_sets_subseteq)
+ also have "\<dots> \<subseteq> sigma_sets ?O ?G" by (rule sigma_sets_superset_generator)
finally show "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> sigma_sets ?O ?G" .
have "emb I J ` sets (Pi\<^isub>M J M) = emb I J ` sigma_sets (space (Pi\<^isub>M J M)) (Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)
--- a/src/HOL/Probability/Probability_Measure.thy Wed Jul 06 13:52:42 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Wed Jul 06 13:57:52 2011 +0200
@@ -1107,43 +1107,44 @@
by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1)
qed
-subsection "Borel Measure on {0 .. 1}"
+subsection "Borel Measure on {0 ..< 1}"
definition pborel :: "real measure_space" where
- "pborel = lborel.restricted_space {0 .. 1}"
+ "pborel = lborel.restricted_space {0 ..< 1}"
lemma space_pborel[simp]:
- "space pborel = {0 .. 1}"
+ "space pborel = {0 ..< 1}"
unfolding pborel_def by auto
lemma sets_pborel:
- "A \<in> sets pborel \<longleftrightarrow> A \<in> sets borel \<and> A \<subseteq> { 0 .. 1}"
+ "A \<in> sets pborel \<longleftrightarrow> A \<in> sets borel \<and> A \<subseteq> { 0 ..< 1}"
unfolding pborel_def by auto
lemma in_pborel[intro, simp]:
- "A \<subseteq> {0 .. 1} \<Longrightarrow> A \<in> sets borel \<Longrightarrow> A \<in> sets pborel"
+ "A \<subseteq> {0 ..< 1} \<Longrightarrow> A \<in> sets borel \<Longrightarrow> A \<in> sets pborel"
unfolding pborel_def by auto
interpretation pborel: measure_space pborel
- using lborel.restricted_measure_space[of "{0 .. 1}"]
+ using lborel.restricted_measure_space[of "{0 ..< 1}"]
by (simp add: pborel_def)
interpretation pborel: prob_space pborel
by default (simp add: one_extreal_def pborel_def)
-lemma pborel_prob: "pborel.prob A = (if A \<in> sets borel \<and> A \<subseteq> {0 .. 1} then real (lborel.\<mu> A) else 0)"
+lemma pborel_prob: "pborel.prob A = (if A \<in> sets borel \<and> A \<subseteq> {0 ..< 1} then real (lborel.\<mu> A) else 0)"
unfolding pborel.\<mu>'_def by (auto simp: pborel_def)
lemma pborel_singelton[simp]: "pborel.prob {a} = 0"
by (auto simp: pborel_prob)
lemma
- shows pborel_atLeastAtMost[simp]: "pborel.\<mu>' {a .. b} = (if 0 \<le> a \<and> a \<le> b \<and> b \<le> 1 then b - a else 0)"
+ shows pborel_atLeastAtMost[simp]: "pborel.\<mu>' {a .. b} = (if 0 \<le> a \<and> a \<le> b \<and> b < 1 then b - a else 0)"
and pborel_atLeastLessThan[simp]: "pborel.\<mu>' {a ..< b} = (if 0 \<le> a \<and> a \<le> b \<and> b \<le> 1 then b - a else 0)"
- and pborel_greaterThanAtMost[simp]: "pborel.\<mu>' {a <.. b} = (if 0 \<le> a \<and> a \<le> b \<and> b \<le> 1 then b - a else 0)"
+ and pborel_greaterThanAtMost[simp]: "pborel.\<mu>' {a <.. b} = (if 0 \<le> a \<and> a \<le> b \<and> b < 1 then b - a else 0)"
and pborel_greaterThanLessThan[simp]: "pborel.\<mu>' {a <..< b} = (if 0 \<le> a \<and> a \<le> b \<and> b \<le> 1 then b - a else 0)"
- unfolding pborel_prob by (auto simp: atLeastLessThan_subseteq_atLeastAtMost_iff
- greaterThanAtMost_subseteq_atLeastAtMost_iff greaterThanLessThan_subseteq_atLeastAtMost_iff)
+ unfolding pborel_prob
+ by (auto simp: atLeastAtMost_subseteq_atLeastLessThan_iff
+ greaterThanAtMost_subseteq_atLeastLessThan_iff greaterThanLessThan_subseteq_atLeastLessThan_iff)
lemma pborel_lebesgue_measure:
"A \<in> sets pborel \<Longrightarrow> pborel.prob A = real (measure lebesgue A)"
@@ -1151,16 +1152,16 @@
lemma pborel_alt:
"pborel = sigma \<lparr>
- space = {0..1},
- sets = range (\<lambda>(x,y). {x..y} \<inter> {0..1}),
+ space = {0..<1},
+ sets = range (\<lambda>(x,y). {x..<y} \<inter> {0..<1}),
measure = measure lborel \<rparr>" (is "_ = ?R")
proof -
- have *: "{0..1::real} \<in> sets borel" by auto
- have **: "op \<inter> {0..1::real} ` range (\<lambda>(x, y). {x..y}) = range (\<lambda>(x,y). {x..y} \<inter> {0..1})"
+ have *: "{0..<1::real} \<in> sets borel" by auto
+ have **: "op \<inter> {0..<1::real} ` range (\<lambda>(x, y). {x..<y}) = range (\<lambda>(x,y). {x..<y} \<inter> {0..<1})"
unfolding image_image by (intro arg_cong[where f=range]) auto
- have "pborel = algebra.restricted_space (sigma \<lparr>space=UNIV, sets=range (\<lambda>(a, b). {a .. b :: real}),
- measure = measure pborel\<rparr>) {0 .. 1}"
- by (simp add: sigma_def lebesgue_def pborel_def borel_eq_atLeastAtMost lborel_def)
+ have "pborel = algebra.restricted_space (sigma \<lparr>space=UNIV, sets=range (\<lambda>(a, b). {a ..< b :: real}),
+ measure = measure pborel\<rparr>) {0 ..< 1}"
+ by (simp add: sigma_def lebesgue_def pborel_def borel_eq_atLeastLessThan lborel_def)
also have "\<dots> = ?R"
by (subst restricted_sigma)
(simp_all add: sets_sigma sigma_sets.Basic ** pborel_def image_eqI[of _ _ "(0,1)"])
--- a/src/HOL/SetInterval.thy Wed Jul 06 13:52:42 2011 +0200
+++ b/src/HOL/SetInterval.thy Wed Jul 06 13:57:52 2011 +0200
@@ -284,6 +284,21 @@
using dense[of "a" "min c b"] dense[of "max a d" "b"]
by (force simp: subset_eq Ball_def not_less[symmetric])
+lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
+ "{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)"
+ using dense[of "max a d" "b"]
+ by (force simp: subset_eq Ball_def not_less[symmetric])
+
+lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:
+ "{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)"
+ using dense[of "a" "min c b"]
+ by (force simp: subset_eq Ball_def not_less[symmetric])
+
+lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:
+ "{a <..< b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
+ using dense[of "a" "min c b"] dense[of "max a d" "b"]
+ by (force simp: subset_eq Ball_def not_less[symmetric])
+
end
lemma (in linorder) atLeastLessThan_subset_iff:
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Jul 06 13:57:52 2011 +0200
@@ -7,7 +7,9 @@
signature ATP_PROBLEM =
sig
- datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+ datatype ('a, 'b) ho_term =
+ ATerm of 'a * ('a, 'b) ho_term list |
+ AAbs of ('a * 'b) * ('a, 'b) ho_term
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIff
datatype ('a, 'b, 'c) formula =
@@ -21,8 +23,8 @@
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
- Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
- * string fo_term option * string fo_term option
+ Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
+ * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
type 'a problem = (string * 'a problem_line list) list
val tptp_cnf : string
@@ -36,7 +38,9 @@
val tptp_fun_type : string
val tptp_product_type : string
val tptp_forall : string
+ val tptp_ho_forall : string
val tptp_exists : string
+ val tptp_ho_exists : string
val tptp_not : string
val tptp_and : string
val tptp_or : string
@@ -91,7 +95,9 @@
(** ATP problem **)
-datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+datatype ('a, 'b) ho_term =
+ ATerm of 'a * ('a, 'b) ho_term list |
+ AAbs of ('a * 'b) * ('a, 'b) ho_term
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIff
datatype ('a, 'b, 'c) formula =
@@ -105,8 +111,8 @@
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
- Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
- * string fo_term option * string fo_term option
+ Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
+ * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
type 'a problem = (string * 'a problem_line list) list
(* official TPTP syntax *)
@@ -121,7 +127,9 @@
val tptp_fun_type = ">"
val tptp_product_type = "*"
val tptp_forall = "!"
+val tptp_ho_forall = "!!"
val tptp_exists = "?"
+val tptp_ho_exists = "??"
val tptp_not = "~"
val tptp_and = "&"
val tptp_or = "|"
@@ -225,6 +233,9 @@
else
s ^ "(" ^ commas ss ^ ")"
end
+ | string_for_term THF (AAbs ((s, ty), tm)) =
+ "(^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm ^ ")"
+ | string_for_term _ _ = raise Fail "unexpected term in first-order format"
fun string_for_quantifier AForall = tptp_forall
| string_for_quantifier AExists = tptp_exists
@@ -303,8 +314,9 @@
| is_problem_line_cnf_ueq _ = false
fun open_conjecture_term (ATerm ((s, s'), tms)) =
- ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
- else (s, s'), tms |> map open_conjecture_term)
+ ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
+ else (s, s'), tms |> map open_conjecture_term)
+ | open_conjecture_term _ = raise Fail "unexpected higher-order term"
fun open_formula conj =
let
(* We are conveniently assuming that all bound variable names are
@@ -403,9 +415,10 @@
fun do_type (AFun (ty1, ty2)) = fold do_type [ty1, ty2]
| do_type (AType name) = do_sym name (K atype_of_types)
fun do_term pred_sym (ATerm (name as (s, _), tms)) =
- is_tptp_user_symbol s
- ? do_sym name (fn _ => default_type pred_sym (length tms))
- #> fold (do_term false) tms
+ is_tptp_user_symbol s
+ ? do_sym name (fn _ => default_type pred_sym (length tms))
+ #> fold (do_term false) tms
+ | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
fun do_formula (AQuant (_, xs, phi)) =
fold do_type (map_filter snd xs) #> do_formula phi
| do_formula (AConn (_, phis)) = fold do_formula phis
@@ -496,10 +509,12 @@
end
in add 0 |> apsnd SOME end
-fun nice_term (ATerm (name, ts)) =
- nice_name name ##>> pool_map nice_term ts #>> ATerm
fun nice_type (AType name) = nice_name name #>> AType
| nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
+fun nice_term (ATerm (name, ts)) =
+ nice_name name ##>> pool_map nice_term ts #>> ATerm
+ | nice_term (AAbs ((name, ty), tm)) =
+ nice_name name ##>> nice_type ty ##>> nice_term tm #>> AAbs
fun nice_formula (AQuant (q, xs, phi)) =
pool_map nice_name (map fst xs)
##>> pool_map (fn NONE => pair NONE
--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 06 13:57:52 2011 +0200
@@ -8,7 +8,7 @@
signature ATP_PROOF =
sig
- type 'a fo_term = 'a ATP_Problem.fo_term
+ type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
type 'a problem = 'a ATP_Problem.problem
@@ -41,7 +41,7 @@
Definition of step_name * 'a * 'a |
Inference of step_name * 'a * step_name list
- type 'a proof = ('a, 'a, 'a fo_term) formula step list
+ type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
val short_output : bool -> string -> string
val string_for_failure : failure -> string
@@ -54,7 +54,7 @@
val is_same_atp_step : step_name -> step_name -> bool
val scan_general_id : string list -> string * string list
val parse_formula :
- string list -> (string, 'a, string fo_term) formula * string list
+ string list -> (string, 'a, (string, 'a) ho_term) formula * string list
val atp_proof_from_tstplike_proof :
string problem -> string -> string -> string proof
val clean_up_atp_proof_dependencies : string proof -> string proof
@@ -228,7 +228,7 @@
Definition of step_name * 'a * 'a |
Inference of step_name * 'a * step_name list
-type 'a proof = ('a, 'a, 'a fo_term) formula step list
+type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
fun step_name (Definition (name, _, _)) = name
| step_name (Inference (name, _, _)) = name
@@ -293,7 +293,7 @@
| (u1, SOME (SOME _, u2)) =>
mk_anot (AAtom (ATerm ("equal", [u1, u2]))))) x
-fun fo_term_head (ATerm (s, _)) = s
+fun ho_term_head (ATerm (s, _)) = s
(* TPTP formulas are fully parenthesized, so we don't need to worry about
operator precedence. *)
@@ -325,7 +325,7 @@
--| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
>> (fn ((q, ts), phi) =>
(* We ignore TFF and THF types for now. *)
- AQuant (q, map (rpair NONE o fo_term_head) ts, phi))) x
+ AQuant (q, map (rpair NONE o ho_term_head) ts, phi))) x
fun skip_formula ss =
let
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Jul 06 13:57:52 2011 +0200
@@ -8,7 +8,7 @@
signature ATP_RECONSTRUCT =
sig
- type 'a fo_term = 'a ATP_Problem.fo_term
+ type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
type 'a proof = 'a ATP_Proof.proof
type locality = ATP_Translate.locality
@@ -41,11 +41,11 @@
val make_tvar : string -> typ
val make_tfree : Proof.context -> string -> typ
val term_from_atp :
- Proof.context -> bool -> int Symtab.table -> typ option -> string fo_term
+ Proof.context -> bool -> int Symtab.table -> typ option -> (string, string) ho_term
-> term
val prop_from_atp :
Proof.context -> bool -> int Symtab.table
- -> (string, string, string fo_term) formula -> term
+ -> (string, string, (string, string) ho_term) formula -> term
val isar_proof_text :
Proof.context -> bool -> isar_params -> one_line_params -> string
val proof_text :
@@ -304,8 +304,8 @@
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
-exception FO_TERM of string fo_term list
-exception FORMULA of (string, string, string fo_term) formula list
+exception HO_TERM of (string, string) ho_term list
+exception FORMULA of (string, string, (string, string) ho_term) formula list
exception SAME of unit
(* Type variables are given the basic sort "HOL.type". Some will later be
@@ -316,7 +316,7 @@
SOME b => Type (invert_const b, Ts)
| NONE =>
if not (null us) then
- raise FO_TERM [u] (* only "tconst"s have type arguments *)
+ raise HO_TERM [u] (* only "tconst"s have type arguments *)
else case strip_prefix_and_unascii tfree_prefix a of
SOME b => make_tfree ctxt b
| NONE =>
@@ -333,7 +333,7 @@
fun type_constraint_from_term ctxt (u as ATerm (a, us)) =
case (strip_prefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
(SOME b, [T]) => (b, T)
- | _ => raise FO_TERM [u]
+ | _ => raise HO_TERM [u]
(** Accumulate type constraints in a formula: negative type literals **)
fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
@@ -393,7 +393,7 @@
case mangled_us @ us of
[typ_u, term_u] =>
do_term extra_ts (SOME (typ_from_atp ctxt typ_u)) term_u
- | _ => raise FO_TERM us
+ | _ => raise HO_TERM us
else if s' = predicator_name then
do_term [] (SOME @{typ bool}) (hd us)
else if s' = app_op_name then
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jul 06 13:57:52 2011 +0200
@@ -8,7 +8,7 @@
signature ATP_TRANSLATE =
sig
- type 'a fo_term = 'a ATP_Problem.fo_term
+ type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
type connective = ATP_Problem.connective
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
type format = ATP_Problem.format
@@ -83,7 +83,7 @@
val choose_format : format list -> type_enc -> format * type_enc
val mk_aconns :
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
- val unmangled_const : string -> string * string fo_term list
+ val unmangled_const : string -> string * (string, 'b) ho_term list
val unmangled_const_name : string -> string
val helper_table : ((string * bool) * thm list) list
val factsN : string
@@ -229,7 +229,11 @@
("c_implies", (@{const_name implies}, (@{thm fimplies_def},
("fimplies", @{const_name ATP.fimplies})))),
("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
- ("fequal", @{const_name ATP.fequal}))))]
+ ("fequal", @{const_name ATP.fequal})))),
+ ("c_All", (@{const_name All}, (@{thm fAll_def},
+ ("fAll", @{const_name ATP.fAll})))),
+ ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
+ ("fEx", @{const_name ATP.fEx}))))]
val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
@@ -245,6 +249,8 @@
(@{const_name disj}, "disj"),
(@{const_name implies}, "implies"),
(@{const_name HOL.eq}, "equal"),
+ (@{const_name All}, "All"),
+ (@{const_name Ex}, "Ex"),
(@{const_name If}, "If"),
(@{const_name Set.member}, "member"),
(@{const_name Meson.COMBI}, "COMBI"),
@@ -442,11 +448,13 @@
datatype combterm =
CombConst of name * typ * typ list |
CombVar of name * typ |
- CombApp of combterm * combterm
+ CombApp of combterm * combterm |
+ CombAbs of (name * typ) * combterm
fun combtyp_of (CombConst (_, T, _)) = T
| combtyp_of (CombVar (_, T)) = T
| combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
+ | combtyp_of (CombAbs ((_, T), tm)) = T --> combtyp_of tm
(*gets the head of a combinator application, along with the list of arguments*)
fun strip_combterm_comb u =
@@ -490,7 +498,15 @@
| combterm_from_term _ bs (Bound j) =
nth bs j
|> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
- | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
+ | combterm_from_term thy bs (Abs (s, T, t)) =
+ let
+ fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
+ val s = vary s
+ val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t
+ in
+ (CombAbs ((`make_bound_var s, T), tm),
+ union (op =) atomic_Ts (atyps_of T))
+ end
datatype locality =
General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
@@ -545,7 +561,8 @@
("simple", (NONE, _, Lightweight)) =>
Simple_Types (First_Order, level)
| ("simple_higher", (NONE, _, Lightweight)) =>
- Simple_Types (Higher_Order, level)
+ if level = Noninf_Nonmono_Types then raise Same.SAME
+ else Simple_Types (Higher_Order, level)
| ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
| ("tags", (SOME Polymorphic, _, _)) =>
Tags (Polymorphic, level, heaviness)
@@ -696,16 +713,19 @@
fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
| combterm_vars (CombConst _) = I
| combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
+ | combterm_vars (CombAbs (_, tm)) = combterm_vars tm
fun close_combformula_universally phi = close_universally combterm_vars phi
-fun term_vars (ATerm (name as (s, _), tms)) =
- is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
-fun close_formula_universally phi = close_universally term_vars phi
+fun term_vars bounds (ATerm (name as (s, _), tms)) =
+ (is_tptp_variable s andalso not (member (op =) bounds name))
+ ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms
+ | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm
+fun close_formula_universally phi = close_universally (term_vars []) phi
val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
val homo_infinite_type = Type (homo_infinite_type_name, [])
-fun fo_term_from_typ format type_enc =
+fun ho_term_from_typ format type_enc =
let
fun term (Type (s, Ts)) =
ATerm (case (is_type_enc_higher_order type_enc, s) of
@@ -722,8 +742,8 @@
ATerm ((make_schematic_type_var x, s), [])
in term end
-fun fo_term_for_type_arg format type_enc T =
- if T = dummyT then NONE else SOME (fo_term_from_typ format type_enc T)
+fun ho_term_for_type_arg format type_enc T =
+ if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
(* This shouldn't clash with anything else. *)
val mangled_type_sep = "\000"
@@ -732,6 +752,7 @@
| generic_mangled_type_name f (ATerm (name, tys)) =
f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
^ ")"
+ | generic_mangled_type_name f _ = raise Fail "unexpected type abstraction"
val bool_atype = AType (`I tptp_bool_type)
@@ -742,7 +763,7 @@
else
simple_type_prefix ^ ascii_of s
-fun ho_type_from_fo_term type_enc pred_sym ary =
+fun ho_type_from_ho_term type_enc pred_sym ary =
let
fun to_atype ty =
AType ((make_simple_type (generic_mangled_type_name fst ty),
@@ -750,17 +771,19 @@
fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
| to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
+ | to_fo ary _ = raise Fail "unexpected type abstraction"
fun to_ho (ty as ATerm ((s, _), tys)) =
- if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
+ if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
+ | to_ho _ = raise Fail "unexpected type abstraction"
in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
-fun mangled_type format type_enc pred_sym ary =
- ho_type_from_fo_term type_enc pred_sym ary
- o fo_term_from_typ format type_enc
+fun ho_type_from_typ format type_enc pred_sym ary =
+ ho_type_from_ho_term type_enc pred_sym ary
+ o ho_term_from_typ format type_enc
fun mangled_const_name format type_enc T_args (s, s') =
let
- val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_enc)
+ val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
fun type_suffix f g =
fold_rev (curry (op ^) o g o prefix mangled_type_sep
o generic_mangled_type_name f) ty_args ""
@@ -804,6 +827,8 @@
| (false, "c_conj") => (`I tptp_and, [])
| (false, "c_disj") => (`I tptp_or, [])
| (false, "c_implies") => (`I tptp_implies, [])
+ | (false, "c_All") => (`I tptp_ho_forall, [])
+ | (false, "c_Ex") => (`I tptp_ho_exists, [])
| (false, s) =>
if is_tptp_equal s then (`I tptp_equal, [])
else (proxy_base |>> prefix const_prefix, T_args)
@@ -812,6 +837,7 @@
(proxy_base |>> prefix const_prefix, T_args)
| NONE => (name, T_args))
|> (fn (name, T_args) => CombConst (name, T, T_args))
+ | intro _ (CombAbs (bound, tm)) = CombAbs (bound, intro false tm)
| intro _ tm = tm
in intro true end
@@ -872,7 +898,7 @@
else
t
-fun introduce_combinators_in_term ctxt kind t =
+fun process_abstractions_in_term ctxt type_enc kind t =
let val thy = Proof_Context.theory_of ctxt in
if Meson.is_fol_term thy t then
t
@@ -897,6 +923,8 @@
t0 $ aux Ts t1 $ aux Ts t2
| _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
t
+ else if is_type_enc_higher_order type_enc then
+ t |> Envir.eta_contract
else
t |> conceal_bounds Ts
|> Envir.eta_contract
@@ -923,7 +951,7 @@
| aux t = t
in t |> exists_subterm is_Var t ? aux end
-fun preprocess_prop ctxt presimp_consts kind t =
+fun preprocess_prop ctxt type_enc presimp_consts kind t =
let
val thy = Proof_Context.theory_of ctxt
val t = t |> Envir.beta_eta_contract
@@ -936,7 +964,7 @@
|> extensionalize_term ctxt
|> presimplify_term ctxt presimp_consts
|> perhaps (try (HOLogic.dest_Trueprop))
- |> introduce_combinators_in_term ctxt kind
+ |> process_abstractions_in_term ctxt type_enc kind
end
(* making fact and conjecture formulas *)
@@ -952,7 +980,7 @@
fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
((name, loc), t) =
let val thy = Proof_Context.theory_of ctxt in
- case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
+ case t |> preproc ? preprocess_prop ctxt type_enc presimp_consts Axiom
|> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
loc Axiom of
formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
@@ -976,7 +1004,7 @@
else I)
in
t |> preproc ?
- (preprocess_prop ctxt presimp_consts kind #> freeze_term)
+ (preprocess_prop ctxt type_enc presimp_consts kind #> freeze_term)
|> make_formula thy type_enc (format <> CNF) (string_of_int j)
Local kind
|> maybe_negate
@@ -1125,6 +1153,8 @@
end)
end
| CombVar (_, T) => add_var_or_bound_var T accum
+ | CombAbs ((_, T), tm) =>
+ accum |> add_var_or_bound_var T |> add false tm
| _ => accum)
|> fold (add false) args
end
@@ -1254,6 +1284,7 @@
| No_Type_Args => (name, [])
end)
|> (fn (name, T_args) => CombConst (name, T, T_args))
+ | aux _ (CombAbs (bound, tm)) = CombAbs (bound, aux 0 tm)
| aux _ tm = tm
in aux 0 end
@@ -1275,12 +1306,6 @@
(("COMBB", false), @{thms Meson.COMBB_def}),
(("COMBC", false), @{thms Meson.COMBC_def}),
(("COMBS", false), @{thms Meson.COMBS_def}),
- (("fequal", true),
- (* This is a lie: Higher-order equality doesn't need a sound type encoding.
- However, this is done so for backward compatibility: Including the
- equality helpers by default in Metis breaks a few existing proofs. *)
- @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
- fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
(("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
(("fFalse", true), @{thms True_or_False}),
(("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
@@ -1297,6 +1322,14 @@
(("fimplies", false),
@{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
by (unfold fimplies_def) fast+}),
+ (("fequal", true),
+ (* This is a lie: Higher-order equality doesn't need a sound type encoding.
+ However, this is done so for backward compatibility: Including the
+ equality helpers by default in Metis breaks a few existing proofs. *)
+ @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
+ fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
+ (("fAll", false), []), (*TODO: add helpers*)
+ (("fEx", false), []), (*TODO: add helpers*)
(("If", true), @{thms if_True if_False True_or_False})]
|> map (apsnd (map zero_var_indexes))
@@ -1444,36 +1477,41 @@
fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
| is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
+ | is_var_positively_naked_in_term name _ _ _ = true
fun should_predicate_on_var_in_formula pos phi (SOME true) name =
formula_fold pos (is_var_positively_naked_in_term name) phi false
| should_predicate_on_var_in_formula _ _ _ _ = true
-fun mk_const_aterm format type_enc x T_args args =
- ATerm (x, map_filter (fo_term_for_type_arg format type_enc) T_args @ args)
+fun mk_aterm format type_enc name T_args args =
+ ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
CombConst (type_tag, T --> T, [T])
|> enforce_type_arg_policy_in_combterm ctxt format type_enc
- |> term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
+ |> ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
|> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
-and term_from_combterm ctxt format nonmono_Ts type_enc =
+and ho_term_from_combterm ctxt format nonmono_Ts type_enc =
let
fun aux site u =
let
val (head, args) = strip_combterm_comb u
- val (x as (s, _), T_args) =
- case head of
- CombConst (name, _, T_args) => (name, T_args)
- | CombVar (name, _) => (name, [])
- | CombApp _ => raise Fail "impossible \"CombApp\""
- val (pos, arg_site) =
+ val pos =
case site of
- Top_Level pos =>
- (pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
- | Eq_Arg pos => (pos, Elsewhere)
- | Elsewhere => (NONE, Elsewhere)
- val t = mk_const_aterm format type_enc x T_args
- (map (aux arg_site) args)
+ Top_Level pos => pos
+ | Eq_Arg pos => pos
+ | Elsewhere => NONE
+ val t =
+ case head of
+ CombConst (name as (s, _), _, T_args) =>
+ let
+ val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
+ in
+ mk_aterm format type_enc name T_args (map (aux arg_site) args)
+ end
+ | CombVar (name, _) => mk_aterm format type_enc name [] (map (aux Elsewhere) args)
+ | CombAbs ((name, T), tm) =>
+ AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm)
+ | CombApp _ => raise Fail "impossible \"CombApp\""
val T = combtyp_of u
in
t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
@@ -1486,12 +1524,12 @@
should_predicate_on_var =
let
fun do_term pos =
- term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
+ ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
val do_bound_type =
case type_enc of
Simple_Types (_, level) =>
homogenized_type ctxt nonmono_Ts level 0
- #> mangled_type format type_enc false 0 #> SOME
+ #> ho_type_from_typ format type_enc false 0 #> SOME
| _ => K NONE
fun do_out_of_bound_type pos phi universal (name, T) =
if should_predicate_on_type ctxt nonmono_Ts type_enc
@@ -1614,6 +1652,7 @@
else
I
end
+ | CombAbs (_, tm) => add_combterm in_conj tm
| _ => I)
#> fold (add_combterm in_conj) args
end
@@ -1666,7 +1705,7 @@
in
Decl (sym_decl_prefix ^ s, (s, s'),
(T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
- |> mangled_type format type_enc pred_sym (length T_arg_Ts + ary))
+ |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
end
fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
@@ -1716,7 +1755,7 @@
val bound_names =
1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
val bounds = bound_names |> map (fn name => ATerm (name, []))
- val cst = mk_const_aterm format type_enc (s, s') T_args
+ val cst = mk_aterm format type_enc (s, s') T_args
val atomic_Ts = atyps_of T
fun eq tms =
(if pred_sym then AConn (AIff, map AAtom tms)
@@ -1924,8 +1963,9 @@
val type_info_default_weight = 0.8
fun add_term_weights weight (ATerm (s, tms)) =
- is_tptp_user_symbol s ? Symtab.default (s, weight)
- #> fold (add_term_weights weight) tms
+ is_tptp_user_symbol s ? Symtab.default (s, weight)
+ #> fold (add_term_weights weight) tms
+ | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
formula_fold NONE (K (add_term_weights weight)) phi
| add_problem_line_weights _ _ = I
--- a/src/HOL/Tools/Quotient/quotient_def.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Wed Jul 06 13:57:52 2011 +0200
@@ -46,8 +46,9 @@
fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
let
val (vars, ctxt) = prep_vars (the_list raw_var) lthy
- val lhs = prep_term ctxt lhs_raw
- val rhs = prep_term ctxt rhs_raw
+ val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
+ val lhs = prep_term T_opt ctxt lhs_raw
+ val rhs = prep_term NONE ctxt rhs_raw
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
@@ -80,8 +81,12 @@
(qconst_data, lthy'')
end
-val quotient_def = gen_quotient_def Proof_Context.cert_vars Syntax.check_term
-val quotdef_cmd = gen_quotient_def Proof_Context.read_vars Syntax.read_term
+fun check_term' cnstr ctxt =
+ Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
+fun read_term' cnstr ctxt = check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
+
+val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
+val quotdef_cmd = gen_quotient_def Proof_Context.read_vars read_term'
(* a wrapper for automatically lifting a raw constant *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/counter.scala Wed Jul 06 13:57:52 2011 +0200
@@ -0,0 +1,27 @@
+/* Title: Pure/Concurrent/counter.scala
+ Author: Makarius
+
+Synchronized counter for unique identifiers < 0.
+
+NB: ML ticks forwards, JVM ticks backwards.
+*/
+
+package isabelle
+
+
+object Counter
+{
+ type ID = Long
+}
+
+class Counter
+{
+ private var count: Counter.ID = 0
+
+ def apply(): Counter.ID = synchronized {
+ require(count > java.lang.Long.MIN_VALUE)
+ count -= 1
+ count
+ }
+}
+
--- a/src/Pure/Concurrent/future.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Jul 06 13:57:52 2011 +0200
@@ -584,9 +584,9 @@
(case worker_task () of
NONE => I
| SOME task => Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]);
- val _ = Output.status (Markup.markup (task_props Markup.forked) "");
+ val _ = Output.status (Markup.markup_only (task_props Markup.forked));
val x = e (); (*sic -- report "joined" only for success*)
- val _ = Output.status (Markup.markup (task_props Markup.joined) "");
+ val _ = Output.status (Markup.markup_only (task_props Markup.joined));
in x end;
--- a/src/Pure/General/markup.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/General/markup.ML Wed Jul 06 13:57:52 2011 +0200
@@ -92,6 +92,7 @@
val command_spanN: string val command_span: string -> T
val ignored_spanN: string val ignored_span: T
val malformed_spanN: string val malformed_span: T
+ val loaded_theoryN: string val loaded_theory: string -> T
val elapsedN: string
val cpuN: string
val gcN: string
@@ -110,7 +111,7 @@
val versionN: string
val execN: string
val assignN: string val assign: int -> T
- val editN: string val edit: int -> int -> T
+ val editN: string val edit: int * int -> T
val serialN: string
val promptN: string val prompt: T
val readyN: string val ready: T
@@ -123,6 +124,7 @@
val output: T -> Output.output * Output.output
val enclose: T -> Output.output -> Output.output
val markup: T -> string -> string
+ val markup_only: T -> string
end;
structure Markup: MARKUP =
@@ -304,6 +306,11 @@
val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
+(* theory loader *)
+
+val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" nameN;
+
+
(* timing *)
val timingN = "timing";
@@ -347,7 +354,7 @@
val (assignN, assign) = markup_int "assign" versionN;
val editN = "edit";
-fun edit cmd_id exec_id : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
+fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
(* messages *)
@@ -387,4 +394,6 @@
let val (bg, en) = output m
in Library.enclose (Output.escape bg) (Output.escape en) end;
+fun markup_only m = markup m "";
+
end;
--- a/src/Pure/General/markup.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/General/markup.scala Wed Jul 06 13:57:52 2011 +0200
@@ -246,6 +246,11 @@
val MALFORMED_SPAN = "malformed_span"
+ /* theory loader */
+
+ val LOADED_THEORY = "loaded_theory"
+
+
/* timing */
val TIMING = "timing"
--- a/src/Pure/General/path.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/General/path.scala Wed Jul 06 13:57:52 2011 +0200
@@ -19,7 +19,7 @@
private case object Parent extends Elem
private def err_elem(msg: String, s: String): Nothing =
- error (msg + " path element specification: " + Library.quote(s))
+ error (msg + " path element specification: " + quote(s))
private def check_elem(s: String): String =
if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
@@ -27,7 +27,7 @@
s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
case Nil => s
case bads =>
- err_elem ("Illegal character(s) " + Library.commas_quote(bads.map(_.toString)) + " in", s)
+ err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)
}
private def root_elem(s: String): Elem = Root(check_elem(s))
@@ -82,7 +82,7 @@
def explode(str: String): Path =
{
- val ss = Library.space_explode('/', str)
+ val ss = space_explode('/', str)
val r = ss.takeWhile(_.isEmpty).length
val es = ss.dropWhile(_.isEmpty)
val (roots, raw_elems) =
@@ -92,8 +92,12 @@
else (List(root_elem(es.head)), es.tail)
Path(norm_elems(explode_elems(raw_elems) ++ roots))
}
+
+ def split(str: String): List[Path] =
+ space_explode(':', str).filterNot(_.isEmpty).map(explode)
}
+
class Path
{
protected val elems: List[Path.Elem] = Nil // reversed elements
@@ -114,7 +118,7 @@
case _ => elems.map(Path.implode_elem).reverse.mkString("/")
}
- override def toString: String = Library.quote(implode)
+ override def toString: String = quote(implode)
/* base element */
@@ -138,11 +142,12 @@
/* expand */
- def expand(env: String => String): Path =
+ def expand: Path =
{
def eval(elem: Path.Elem): List[Path.Elem] =
elem match {
- case Path.Variable(s) => Path.explode(env(s)).elems
+ case Path.Variable(s) =>
+ Path.explode(Isabelle_System.getenv_strict(s)).elems
case x => List(x)
}
--- a/src/Pure/General/symbol.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/General/symbol.scala Wed Jul 06 13:57:52 2011 +0200
@@ -64,11 +64,11 @@
def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
- def is_physical_newline(s: CharSequence): Boolean =
- "\n".contentEquals(s) || "\r".contentEquals(s) || "\r\n".contentEquals(s)
+ def is_physical_newline(s: String): Boolean =
+ s == "\n" || s == "\r" || s == "\r\n"
- def is_malformed(s: CharSequence): Boolean =
- !(s.length == 1 && is_plain(s.charAt(0))) && malformed_symbol.pattern.matcher(s).matches
+ def is_malformed(s: String): Boolean =
+ !(s.length == 1 && is_plain(s(0))) && malformed_symbol.pattern.matcher(s).matches
class Matcher(text: CharSequence)
{
@@ -87,8 +87,11 @@
/* efficient iterators */
- def iterator(text: CharSequence): Iterator[CharSequence] =
- new Iterator[CharSequence]
+ private val char_symbols: Array[String] =
+ (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
+
+ def iterator(text: CharSequence): Iterator[String] =
+ new Iterator[String]
{
private val matcher = new Matcher(text)
private var i = 0
@@ -96,28 +99,19 @@
def next =
{
val n = matcher(i, text.length)
- val s = text.subSequence(i, i + n)
+ val s =
+ if (n == 0) ""
+ else if (n == 1) {
+ val c = text.charAt(i)
+ if (c < char_symbols.length) char_symbols(c)
+ else text.subSequence(i, i + n).toString
+ }
+ else text.subSequence(i, i + n).toString
i += n
s
}
}
- private val char_symbols: Array[String] =
- (0 until 128).iterator.map(i => new String(Array(i.toChar))).toArray
-
- private def make_string(sym: CharSequence): String =
- sym.length match {
- case 0 => ""
- case 1 =>
- val c = sym.charAt(0)
- if (c < char_symbols.length) char_symbols(c)
- else sym.toString
- case _ => sym.toString
- }
-
- def iterator_string(text: CharSequence): Iterator[String] =
- iterator(text).map(make_string)
-
/* decoding offsets */
--- a/src/Pure/General/yxml.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/General/yxml.scala Wed Jul 06 13:57:52 2011 +0200
@@ -144,12 +144,12 @@
def parse_body_failsafe(source: CharSequence): XML.Body =
{
try { parse_body(source) }
- catch { case _: RuntimeException => List(markup_failsafe(source)) }
+ catch { case ERROR(_) => List(markup_failsafe(source)) }
}
def parse_failsafe(source: CharSequence): XML.Tree =
{
try { parse(source) }
- catch { case _: RuntimeException => markup_failsafe(source) }
+ catch { case ERROR(_) => markup_failsafe(source) }
}
}
--- a/src/Pure/Isar/toplevel.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Jul 06 13:57:52 2011 +0200
@@ -185,8 +185,9 @@
Proof (prf, _) => Proof_Node.position prf
| _ => raise UNDEF);
-fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
- | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
+fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
+ | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos)
+ | end_theory pos (State (NONE, NONE)) = error ("Missing theory " ^ Position.str_of pos);
(* print state *)
@@ -284,6 +285,12 @@
| SOME exn => raise FAILURE (result', exn))
end;
+val exit_transaction =
+ apply_transaction
+ (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (Theory.end_theory thy), NONE)
+ | node => node) (K ())
+ #> (fn State (node', _) => State (NONE, node'));
+
end;
@@ -300,8 +307,8 @@
fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
State (SOME (Theory (Context.Theory
(Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
- | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
- State (NONE, prev)
+ | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
+ exit_transaction state
| apply_tr int (Keep f) state =
Runtime.controlled_execution (fn x => tap (f int) x) state
| apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
@@ -567,7 +574,7 @@
Position.setmp_thread_data pos f x;
fun status tr m =
- setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
+ setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
fun error_msg tr msg =
setmp_thread_position tr (fn () => Output.error_msg msg) ();
--- a/src/Pure/PIDE/command.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/PIDE/command.scala Wed Jul 06 13:57:52 2011 +0200
@@ -80,10 +80,10 @@
/* dummy commands */
def unparsed(source: String): Command =
- new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
+ new Command(Document.no_id, List(Token(Token.Kind.UNPARSED, source)))
def span(toks: List[Token]): Command =
- new Command(Document.NO_ID, toks)
+ new Command(Document.no_id, toks)
}
@@ -97,7 +97,7 @@
def is_ignored: Boolean = span.forall(_.is_ignored)
def is_malformed: Boolean = !is_command && !is_ignored
- def is_unparsed = id == Document.NO_ID
+ def is_unparsed = id == Document.no_id
def name: String = if (is_command) span.head.content else ""
override def toString =
--- a/src/Pure/PIDE/document.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/PIDE/document.ML Wed Jul 06 13:57:52 2011 +0200
@@ -18,7 +18,8 @@
type edit = string * ((command_id option * command_id option) list) option
type state
val init_state: state
- val cancel: state -> unit
+ val get_theory: state -> version_id -> Position.T -> string -> theory
+ val cancel_execution: state -> unit -> unit
val define_command: command_id -> string -> state -> state
val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
val execute: version_id -> state -> state
@@ -49,15 +50,23 @@
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
-abstype node = Node of exec_id option Entries.T (*command entries with excecutions*)
- and version = Version of node Graph.T (*development graph wrt. static imports*)
+abstype node = Node of
+ {last: exec_id, entries: exec_id option Entries.T} (*command entries with excecutions*)
+and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-val empty_node = Node Entries.empty;
-val empty_version = Version Graph.empty;
+fun make_node (last, entries) =
+ Node {last = last, entries = entries};
+
+fun get_last (Node {last, ...}) = last;
+fun set_last last (Node {entries, ...}) = make_node (last, entries);
-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 map_entries f (Node {last, entries}) = make_node (last, f entries);
+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;
+
+val empty_node = make_node (no_id, Entries.empty);
+val empty_version = Version Graph.empty;
(* node edits and associated executions *)
@@ -67,23 +76,22 @@
(*NONE: remove node, SOME: insert/remove commands*)
((command_id option * command_id option) list) option;
-fun the_entry (Node entries) id =
+fun the_entry (Node {entries, ...}) id =
(case Entries.lookup entries id of
NONE => err_undef "command entry" id
| SOME entry => entry);
-fun update_entry (id, exec_id) (Node entries) =
- Node (Entries.update (id, SOME exec_id) entries);
+fun update_entry (id, exec_id) =
+ map_entries (Entries.update (id, SOME exec_id));
fun reset_after id entries =
(case Entries.get_after entries id of
NONE => entries
| SOME next => Entries.update (next, NONE) entries);
-fun edit_node (hook, SOME id2) (Node entries) =
- Node (Entries.insert_after hook (id2, NONE) entries)
- | edit_node (hook, NONE) (Node entries) =
- Node (entries |> Entries.delete_after hook |> reset_after hook);
+val edit_node = map_entries o fold
+ (fn (id, SOME id2) => Entries.insert_after id (id2, NONE)
+ | (id, NONE) => Entries.delete_after id #> reset_after id);
(* version operations *)
@@ -97,7 +105,7 @@
fun edit_nodes (name, SOME edits) (Version nodes) =
Version (nodes
|> Graph.default_node (name, empty_node)
- |> Graph.map_node name (fold edit_node edits))
+ |> Graph.map_node name (edit_node edits))
| edit_nodes (name, NONE) (Version nodes) =
Version (perhaps (try (Graph.del_node name)) nodes);
@@ -182,14 +190,18 @@
NONE => err_undef "command execution" id
| SOME exec => exec);
+fun get_theory state version_id pos name =
+ let
+ val last = get_last (get_node (the_version state version_id) name);
+ val st = #2 (Lazy.force (the_exec state last));
+ in Toplevel.end_theory pos st end;
+
(* document execution *)
-fun cancel (State {execution, ...}) =
- List.app Future.cancel execution;
-
-fun await_cancellation (State {execution, ...}) =
- ignore (Future.join_results execution);
+fun cancel_execution (State {execution, ...}) =
+ (List.app Future.cancel execution;
+ fn () => ignore (Future.join_results execution));
end;
@@ -311,9 +323,9 @@
(case prev of
NONE => no_id
| SOME prev_id => the_default no_id (the_entry node prev_id));
- val (_, rev_upds, st') =
+ val (last, rev_upds, st') =
fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
- val node' = fold update_entry rev_upds node;
+ val node' = node |> fold update_entry rev_upds |> set_last last;
in (rev_upds @ rev_updates, put_node name node' version, st') end)
end;
@@ -338,20 +350,12 @@
fun force_exec NONE = ()
| force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
- val _ = cancel state;
-
val execution' = (* FIXME proper node deps *)
Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
[fn () =>
- let
- val _ = await_cancellation state;
- val _ =
- node_names_of version |> List.app (fn name =>
- fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
- (get_node version name) ());
- in () end];
-
- val _ = await_cancellation state; (* FIXME async!? *)
+ node_names_of version |> List.app (fn name =>
+ fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
+ (get_node version name) ())];
in (versions, commands, execs, execution') end);
--- a/src/Pure/PIDE/document.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/PIDE/document.scala Wed Jul 06 13:57:52 2011 +0200
@@ -27,7 +27,8 @@
type Command_ID = ID
type Exec_ID = ID
- val NO_ID: ID = 0
+ val no_id: ID = 0
+ val new_id = new Counter
@@ -121,7 +122,7 @@
object Version
{
- val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty))
+ val init: Version = new Version(no_id, Map().withDefaultValue(Node.empty))
}
class Version(val id: Version_ID, val nodes: Map[String, Node])
--- a/src/Pure/PIDE/isar_document.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML Wed Jul 06 13:57:52 2011 +0200
@@ -4,12 +4,19 @@
Protocol message formats for interactive Isar documents.
*)
-structure Isar_Document: sig end =
+signature ISAR_DOCUMENT =
+sig
+ val state: unit -> Document.state
+end
+
+structure Isar_Document: ISAR_DOCUMENT =
struct
val global_state = Synchronized.var "Isar_Document" Document.init_state;
val change_state = Synchronized.change global_state;
+fun state () = Synchronized.value global_state;
+
val _ =
Isabelle_Process.add_command "Isar_Document.define_command"
(fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
@@ -30,12 +37,12 @@
(XML_Data.dest_option XML_Data.dest_int)
(XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
- val _ = Document.cancel state;
+ val await_cancellation = Document.cancel_execution state;
val (updates, state') = Document.edit old_id new_id edits state;
+ val _ = await_cancellation ();
val _ =
- implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
- |> Markup.markup (Markup.assign new_id)
- |> Output.status;
+ 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));
--- a/src/Pure/PIDE/text.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/PIDE/text.scala Wed Jul 06 13:57:52 2011 +0200
@@ -46,7 +46,7 @@
def try_restrict(that: Range): Option[Range] =
try { Some (restrict(that)) }
- catch { case _: RuntimeException => None }
+ catch { case ERROR(_) => None }
}
@@ -57,7 +57,7 @@
def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
def try_restrict(r: Text.Range): Option[Info[A]] =
try { Some(Info(range.restrict(r), info)) }
- catch { case _: RuntimeException => None }
+ catch { case ERROR(_) => None }
}
--- a/src/Pure/System/cygwin.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/System/cygwin.scala Wed Jul 06 13:57:52 2011 +0200
@@ -115,7 +115,7 @@
try {
Download.file(parent, "Downloading", new URL("http://www.cygwin.com/setup.exe"), setup_exe)
}
- catch { case _: RuntimeException => error("Failed to download Cygwin setup program") }
+ catch { case ERROR(_) => error("Failed to download Cygwin setup program") }
val (_, rc) = Standard_System.raw_exec(root, null, true,
setup_exe.toString, "-R", root.toString, "-l", download.toString,
--- a/src/Pure/System/gui_setup.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/System/gui_setup.scala Wed Jul 06 13:57:52 2011 +0200
@@ -44,16 +44,15 @@
text.append("JVM name: " + Platform.jvm_name + "\n")
text.append("JVM platform: " + Platform.jvm_platform + "\n")
try {
- val isabelle_system = Isabelle_System.default
- text.append("ML platform: " + isabelle_system.getenv("ML_PLATFORM") + "\n")
- text.append("Isabelle platform: " + isabelle_system.getenv("ISABELLE_PLATFORM") + "\n")
- val platform64 = isabelle_system.getenv("ISABELLE_PLATFORM64")
+ Isabelle_System.init()
+ text.append("ML platform: " + Isabelle_System.getenv("ML_PLATFORM") + "\n")
+ text.append("Isabelle platform: " + Isabelle_System.getenv("ISABELLE_PLATFORM") + "\n")
+ val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64")
if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
- text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
- text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
- } catch {
- case e: RuntimeException => text.append(e.getMessage + "\n")
+ text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n")
+ text.append("Isabelle java: " + Isabelle_System.getenv("THIS_JAVA") + "\n")
}
+ catch { case ERROR(msg) => text.append(msg + "\n") }
// reactions
listenTo(ok)
--- a/src/Pure/System/isabelle_process.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed Jul 06 13:57:52 2011 +0200
@@ -173,11 +173,14 @@
val _ = quick_and_dirty := true;
val _ = Goal.parallel_proofs := 0;
val _ = Context.set_thread_data NONE;
- val _ = Unsynchronized.change print_mode
- (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
+ val _ =
+ Unsynchronized.change print_mode
+ (fold (update op =)
+ [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
val in_stream = setup_channels in_fifo out_fifo;
val _ = Keyword.status ();
+ val _ = Thy_Info.status ();
val _ = Output.status (Markup.markup Markup.ready "process ready");
in loop in_stream end));
--- a/src/Pure/System/isabelle_process.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala Wed Jul 06 13:57:52 2011 +0200
@@ -62,7 +62,7 @@
}
-class Isabelle_Process(system: Isabelle_System, timeout: Time, receiver: Actor, args: String*)
+class Isabelle_Process(timeout: Time, receiver: Actor, args: String*)
{
import Isabelle_Process._
@@ -70,8 +70,7 @@
/* demo constructor */
def this(args: String*) =
- this(Isabelle_System.default, Time.seconds(10),
- actor { loop { react { case res => Console.println(res) } } }, args: _*)
+ this(Time.seconds(10), actor { loop { react { case res => Console.println(res) } } }, args: _*)
/* results */
@@ -93,7 +92,7 @@
private def put_result(kind: String, text: String)
{
- put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
+ put_result(kind, Nil, List(XML.Text(Isabelle_System.symbols.decode(text))))
}
@@ -117,15 +116,16 @@
/** process manager **/
- private val in_fifo = system.mk_fifo()
- private val out_fifo = system.mk_fifo()
- private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
+ private val in_fifo = Isabelle_System.mk_fifo()
+ private val out_fifo = Isabelle_System.mk_fifo()
+ private def rm_fifos() { Isabelle_System.rm_fifo(in_fifo); Isabelle_System.rm_fifo(out_fifo) }
private val process =
try {
val cmdline =
- List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
- new system.Managed_Process(true, cmdline: _*)
+ List(Isabelle_System.getenv_strict("ISABELLE_PROCESS"), "-W",
+ in_fifo + ":" + out_fifo) ++ args
+ new Isabelle_System.Managed_Process(true, cmdline: _*)
}
catch { case e: IOException => rm_fifos(); throw(e) }
@@ -168,8 +168,8 @@
}
else {
// rendezvous
- val command_stream = system.fifo_output_stream(in_fifo)
- val message_stream = system.fifo_input_stream(out_fifo)
+ val command_stream = Isabelle_System.fifo_output_stream(in_fifo)
+ val message_stream = Isabelle_System.fifo_input_stream(out_fifo)
standard_input = stdin_actor()
val stdout = stdout_actor()
@@ -341,7 +341,7 @@
if (i != n) throw new Protocol_Error("bad message chunk content")
- YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
+ YXML.parse_body_failsafe(YXML.decode_chars(Isabelle_System.symbols.decode, buf, 0, n))
//}}}
}
--- a/src/Pure/System/isabelle_system.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Jul 06 13:57:52 2011 +0200
@@ -1,7 +1,8 @@
/* Title: Pure/System/isabelle_system.scala
Author: Makarius
-Isabelle system support (settings environment etc.).
+Fundamental Isabelle system environment: settings, symbols etc.
+Quasi-static module with optional init operation.
*/
package isabelle
@@ -21,15 +22,24 @@
object Isabelle_System
{
- lazy val default: Isabelle_System = new Isabelle_System
-}
+ /** implicit state **/
+
+ private case class State(
+ standard_system: Standard_System,
+ settings: Map[String, String],
+ symbols: Symbol.Interpretation)
+
+ @volatile private var _state: Option[State] = None
-class Isabelle_System(this_isabelle_home: String) extends Standard_System
-{
- def this() = this(null)
+ private def check_state(): State =
+ {
+ if (_state.isEmpty) init() // unsynchronized check
+ _state.get
+ }
-
- /** Isabelle environment **/
+ def standard_system: Standard_System = check_state().standard_system
+ def settings: Map[String, String] = check_state().settings
+ def symbols: Symbol.Interpretation = check_state().symbols
/*
isabelle_home precedence:
@@ -37,50 +47,67 @@
(2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
(3) isabelle.home system property (e.g. via JVM application boot process)
*/
+ def init(this_isabelle_home: String = null) = synchronized {
+ if (_state.isEmpty) {
+ import scala.collection.JavaConversions._
- private val environment: Map[String, String] =
- {
- import scala.collection.JavaConversions._
+ val standard_system = new Standard_System
- val env0 = Map(System.getenv.toList: _*) +
- ("THIS_JAVA" -> this_java())
+ val settings =
+ {
+ val env = Map(System.getenv.toList: _*) +
+ ("THIS_JAVA" -> standard_system.this_java())
- val isabelle_home =
- if (this_isabelle_home != null) this_isabelle_home
- else
- env0.get("ISABELLE_HOME") match {
- case None | Some("") =>
- val path = System.getProperty("isabelle.home")
- if (path == null || path == "") error("Unknown Isabelle home directory")
- else path
- case Some(path) => path
- }
+ val isabelle_home =
+ if (this_isabelle_home != null) this_isabelle_home
+ else
+ env.get("ISABELLE_HOME") match {
+ case None | Some("") =>
+ val path = System.getProperty("isabelle.home")
+ if (path == null || path == "") error("Unknown Isabelle home directory")
+ else path
+ case Some(path) => path
+ }
- Standard_System.with_tmp_file("settings") { dump =>
- val shell_prefix =
- if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil
- val cmdline =
- shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
- val (output, rc) = Standard_System.raw_exec(null, env0, true, cmdline: _*)
- if (rc != 0) error(output)
+ Standard_System.with_tmp_file("settings") { dump =>
+ val shell_prefix =
+ if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
+ else Nil
+ val cmdline =
+ shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
+ val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*)
+ if (rc != 0) error(output)
- val entries =
- for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
- val i = entry.indexOf('=')
- if (i <= 0) (entry -> "")
- else (entry.substring(0, i) -> entry.substring(i + 1))
+ val entries =
+ for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
+ val i = entry.indexOf('=')
+ if (i <= 0) (entry -> "")
+ else (entry.substring(0, i) -> entry.substring(i + 1))
+ }
+ Map(entries: _*) +
+ ("HOME" -> System.getenv("HOME")) +
+ ("PATH" -> System.getenv("PATH"))
+ }
}
- Map(entries: _*) +
- ("HOME" -> System.getenv("HOME")) +
- ("PATH" -> System.getenv("PATH"))
+
+ val symbols =
+ {
+ val isabelle_symbols = settings.getOrElse("ISABELLE_SYMBOLS", "")
+ if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
+ val files =
+ Path.split(isabelle_symbols).map(p => new File(standard_system.jvm_path(p.implode)))
+ new Symbol.Interpretation(split_lines(Standard_System.try_read(files)))
}
+
+ _state = Some(State(standard_system, settings, symbols))
+ }
}
/* getenv */
def getenv(name: String): String =
- environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
+ settings.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
def getenv_strict(name: String): String =
{
@@ -88,19 +115,18 @@
if (value != "") value else error("Undefined environment variable: " + name)
}
- override def toString = getenv_strict("ISABELLE_HOME")
-
-
/** file-system operations **/
/* path specifications */
- def standard_path(path: Path): String = path.expand(getenv_strict).implode
+ def standard_path(path: Path): String = path.expand.implode
- def platform_path(path: Path): String = jvm_path(standard_path(path))
+ def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
def platform_file(path: Path) = new File(platform_path(path))
+ def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
+
/* try_read */
@@ -142,9 +168,9 @@
def execute(redirect: Boolean, args: String*): Process =
{
val cmdline =
- if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
+ if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
else args
- Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
+ Standard_System.raw_execute(null, settings, redirect, cmdline: _*)
}
@@ -239,8 +265,8 @@
def isabelle_tool(name: String, args: String*): (String, Int) =
{
- getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
- val file = platform_file(Path.explode(dir) + Path.basic(name))
+ Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
+ val file = platform_file(dir + Path.basic(name))
try {
file.isFile && file.canRead && file.canExecute &&
!name.endsWith("~") && !name.endsWith(".orig")
@@ -248,7 +274,7 @@
catch { case _: SecurityException => false }
} match {
case Some(dir) =>
- val file = standard_path(Path.explode(dir) + Path.basic(name))
+ val file = standard_path(dir + Path.basic(name))
Standard_System.process_output(execute(true, (List(file) ++ args): _*))
case None => ("Unknown Isabelle tool: " + name, 2)
}
@@ -257,18 +283,13 @@
/* named pipes */
- private var fifo_count: Long = 0
- private def next_fifo(): String = synchronized {
- require(fifo_count < java.lang.Long.MAX_VALUE)
- fifo_count += 1
- fifo_count.toString
- }
+ private val next_fifo = new Counter
def mk_fifo(): String =
{
val i = next_fifo()
val script =
- "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$-" + i + "\"\n" +
+ "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
"echo -n \"$FIFO\"\n" +
"mkfifo -m 600 \"$FIFO\"\n"
val (out, err, rc) = bash(script)
@@ -276,7 +297,7 @@
}
def rm_fifo(fifo: String): Boolean =
- (new File(jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
+ (new File(standard_system.jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
def fifo_input_stream(fifo: String): InputStream =
{
@@ -313,8 +334,8 @@
/* components */
- def components(): List[String] =
- getenv_strict("ISABELLE_COMPONENTS").split(":").toList
+ def components(): List[Path] =
+ Path.split(getenv_strict("ISABELLE_COMPONENTS"))
/* find logics */
@@ -323,8 +344,8 @@
{
val ml_ident = getenv_strict("ML_IDENTIFIER")
val logics = new mutable.ListBuffer[String]
- for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
- val files = platform_file(Path.explode(dir) + Path.explode(ml_ident)).listFiles()
+ for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {
+ val files = platform_file(dir + Path.explode(ml_ident)).listFiles()
if (files != null) {
for (file <- files if file.isFile) logics += file.getName
}
@@ -333,13 +354,6 @@
}
- /* symbols */
-
- val symbols = new Symbol.Interpretation(
- try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList.map(Path.explode))
- .split("\n").toList)
-
-
/* fonts */
def get_font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
@@ -348,7 +362,7 @@
def install_fonts()
{
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
- for (font <- getenv_strict("ISABELLE_FONTS").split(":"))
- ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(Path.explode(font))))
+ for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
+ ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
}
}
--- a/src/Pure/System/session.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/System/session.scala Wed Jul 06 13:57:52 2011 +0200
@@ -2,7 +2,7 @@
Author: Makarius
Options: :folding=explicit:collapseFolds=1:
-Isabelle session, potentially with running prover.
+Main Isabelle/Scala session, potentially with running prover process.
*/
package isabelle
@@ -16,6 +16,14 @@
object Session
{
+ /* abstract file store */
+
+ abstract class File_Store
+ {
+ def read(path: Path): String
+ }
+
+
/* events */
case object Global_Settings
@@ -32,7 +40,7 @@
}
-class Session(val system: Isabelle_System)
+class Session(val file_store: Session.File_Store)
{
/* real time parameters */ // FIXME properties or settings (!?)
@@ -56,17 +64,6 @@
val assignments = new Event_Bus[Session.Assignment.type]
- /* unique ids */
-
- private var id_count: Document.ID = 0
- def new_id(): Document.ID = synchronized {
- require(id_count > java.lang.Long.MIN_VALUE)
- id_count -= 1
- id_count
- }
-
-
-
/** buffered command changes (delay_first discipline) **/
private case object Stop
@@ -116,7 +113,11 @@
/** main protocol actor **/
- @volatile private var syntax = new Outer_Syntax(system.symbols)
+ /* global state */
+
+ @volatile var loaded_theories: Set[String] = Set()
+
+ @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
def current_syntax(): Outer_Syntax = syntax
@volatile private var reverse_syslog = List[XML.Elem]()
@@ -134,15 +135,42 @@
private val global_state = new Volatile(Document.State.init)
def current_state(): Document.State = global_state.peek()
+
+ /* theory files */
+
+ val thy_load = new Thy_Load
+ {
+ override def is_loaded(name: String): Boolean =
+ loaded_theories.contains(name)
+
+ override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
+ {
+ val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
+ if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
+ val text = Standard_System.read_file(file)
+ val header = Thy_Header.read(text)
+ (text, header)
+ }
+ }
+
+ val thy_info = new Thy_Info(thy_load)
+
+
+ /* actor messages */
+
private case object Interrupt_Prover
- private case class Edit_Version(edits: List[Document.Edit_Text])
+ private case class Edit_Node(thy_name: String,
+ header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
+ private case class Init_Node(thy_name: String,
+ header: Exn.Result[Thy_Header.Header], text: String)
private case class Start(timeout: Time, args: List[String])
var verbose: Boolean = false
private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
{
- var prover: Isabelle_Process with Isar_Document = null
+ val this_actor = self
+ var prover: Option[Isabelle_Process with Isar_Document] = None
/* document changes */
@@ -174,7 +202,9 @@
case Some(command) =>
if (global_state.peek().lookup_command(command.id).isEmpty) {
global_state.change(_.define_command(command))
- prover.define_command(command.id, system.symbols.encode(command.source))
+ prover.get.
+ define_command(command.id,
+ Isabelle_System.symbols.encode(command.source))
}
Some(command.id)
}
@@ -183,7 +213,7 @@
(name -> Some(ids))
}
global_state.change(_.define_version(version, former_assignment))
- prover.edit_version(previous.id, version.id, id_edits)
+ prover.get.edit_version(previous.id, version.id, id_edits)
}
//}}}
@@ -230,6 +260,7 @@
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
+ case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
case _ => bad_result(result)
}
}
@@ -241,47 +272,62 @@
//}}}
+ def edit_version(edits: List[Document.Edit_Text])
+ //{{{
+ {
+ val previous = global_state.peek().history.tip.version
+ val syntax = current_syntax()
+ val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, edits) }
+ val change = global_state.change_yield(_.extend_history(previous, edits, result))
+
+ change.version.map(_ => {
+ assignments.await { global_state.peek().is_assigned(previous.get_finished) }
+ this_actor ! change })
+ }
+ //}}}
+
+
/* main loop */
var finished = false
while (!finished) {
receive {
case Interrupt_Prover =>
- if (prover != null) prover.interrupt
+ prover.map(_.interrupt)
- case Edit_Version(edits) if prover != null =>
- val previous = global_state.peek().history.tip.version
- val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
- val change = global_state.change_yield(_.extend_history(previous, edits, result))
-
- val this_actor = self
- change.version.map(_ => {
- assignments.await { global_state.peek().is_assigned(previous.get_finished) }
- this_actor ! change })
-
+ case Edit_Node(thy_name, header, text_edits) if prover.isDefined =>
+ edit_version(List((thy_name, Some(text_edits))))
reply(())
- case change: Document.Change if prover != null => handle_change(change)
+ case Init_Node(thy_name, header, text) if prover.isDefined =>
+ // FIXME compare with existing node
+ edit_version(List(
+ (thy_name, None),
+ (thy_name, Some(List(Text.Edit.insert(0, text))))))
+ reply(())
+
+ case change: Document.Change if prover.isDefined =>
+ handle_change(change)
case result: Isabelle_Process.Result => handle_result(result)
- case Start(timeout, args) if prover == null =>
+ case Start(timeout, args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
- prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
+ prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document)
}
case Stop =>
if (phase == Session.Ready) {
global_state.change(_ => Document.State.init) // FIXME event bus!?
phase = Session.Shutdown
- prover.terminate
+ prover.get.terminate
phase = Session.Inactive
}
finished = true
reply(())
- case bad if prover != null =>
+ case bad if prover.isDefined =>
System.err.println("session_actor: ignoring bad message " + bad)
}
}
@@ -297,7 +343,15 @@
def interrupt() { session_actor ! Interrupt_Prover }
- def edit_version(edits: List[Document.Edit_Text]) { session_actor !? Edit_Version(edits) }
+ def edit_node(thy_name: String, header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
+ {
+ session_actor !? Edit_Node(thy_name, header, edits)
+ }
+
+ def init_node(thy_name: String, header: Exn.Result[Thy_Header.Header], text: String)
+ {
+ session_actor !? Init_Node(thy_name, header, text)
+ }
def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
global_state.peek().snapshot(name, pending_edits)
--- a/src/Pure/System/session_manager.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/System/session_manager.scala Wed Jul 06 13:57:52 2011 +0200
@@ -10,7 +10,7 @@
import java.io.{File, FileFilter}
-class Session_Manager(system: Isabelle_System)
+class Session_Manager
{
val ROOT_NAME = "session.root"
@@ -42,7 +42,7 @@
def component_sessions(): List[List[String]] =
{
val toplevel_sessions =
- system.components().map(s => system.platform_file(Path.explode(s))).filter(is_session_dir)
+ Isabelle_System.components().map(Isabelle_System.platform_file).filter(is_session_dir)
((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
}
}
--- a/src/Pure/System/standard_system.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/System/standard_system.scala Wed Jul 06 13:57:52 2011 +0200
@@ -96,6 +96,16 @@
def read_file(file: File): String = slurp(new FileInputStream(file))
+ def try_read(files: Seq[File]): String =
+ {
+ val buf = new StringBuilder
+ for {
+ file <- files if file.isFile
+ c <- (Source.fromFile(file) ++ Iterator.single('\n'))
+ } buf.append(c)
+ buf.toString
+ }
+
def write_file(file: File, text: CharSequence)
{
val writer =
@@ -254,8 +264,9 @@
class Standard_System
{
+ /* platform_root */
+
val platform_root = if (Platform.is_windows) Cygwin.check_root() else "/"
- override def toString = platform_root
/* jvm_path */
@@ -281,7 +292,7 @@
path
case path => path
}
- for (p <- rest.split("/") if p != "") {
+ for (p <- space_explode('/', rest) if p != "") {
val len = result_path.length
if (len > 0 && result_path(len - 1) != File.separatorChar)
result_path += File.separatorChar
--- a/src/Pure/Thy/html.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/Thy/html.scala Wed Jul 06 13:57:52 2011 +0200
@@ -55,9 +55,10 @@
def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
- def spans(symbols: Symbol.Interpretation,
- input: XML.Tree, original_data: Boolean = false): XML.Body =
+ def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
{
+ val symbols = Isabelle_System.symbols
+
def html_spans(tree: XML.Tree): XML.Body =
tree match {
case XML.Elem(m @ Markup(name, props), ts) =>
@@ -79,7 +80,7 @@
flush()
ts += elem
}
- val syms = Symbol.iterator_string(txt)
+ val syms = Symbol.iterator(txt)
while (syms.hasNext) {
val s1 = syms.next
def s2() = if (syms.hasNext) syms.next else ""
--- a/src/Pure/Thy/thy_header.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala Wed Jul 06 13:57:52 2011 +0200
@@ -9,13 +9,13 @@
import scala.annotation.tailrec
import scala.collection.mutable
-import scala.util.parsing.input.Reader
+import scala.util.parsing.input.{Reader, CharSequenceReader}
import scala.util.matching.Regex
import java.io.File
-object Thy_Header
+object Thy_Header extends Parse.Parser
{
val HEADER = "header"
val THEORY = "theory"
@@ -36,8 +36,10 @@
/* file name */
- val Thy_Path1 = new Regex("([^/]*)\\.thy")
- val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
+ def thy_path(name: String): Path = Path.basic(name).ext("thy")
+
+ private val Thy_Path1 = new Regex("([^/]*)\\.thy")
+ private val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
def split_thy_path(path: String): Option[(String, String)] =
path match {
@@ -45,12 +47,6 @@
case Thy_Path2(dir, name) => Some((dir, name))
case _ => None
}
-}
-
-
-class Thy_Header(symbols: Symbol.Interpretation) extends Parse.Parser
-{
- import Thy_Header._
/* header */
@@ -79,7 +75,7 @@
def read(reader: Reader[Char]): Header =
{
- val token = lexicon.token(symbols, _ => false)
+ val token = lexicon.token(Isabelle_System.symbols, _ => false)
val toks = new mutable.ListBuffer[Token]
@tailrec def scan_to_begin(in: Reader[Char])
@@ -99,10 +95,25 @@
}
}
+ def read(source: CharSequence): Header =
+ read(new CharSequenceReader(source))
+
def read(file: File): Header =
{
val reader = Scan.byte_reader(file)
try { read(reader).decode_permissive_utf8 }
finally { reader.close }
}
+
+
+ /* check */
+
+ def check(name: String, source: CharSequence): Header =
+ {
+ val header = read(source)
+ val name1 = header.name
+ if (name != name1) error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
+ Path.explode(name)
+ header
+ }
}
--- a/src/Pure/Thy/thy_info.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Jul 06 13:57:52 2011 +0200
@@ -10,6 +10,7 @@
datatype action = Update | Remove
val add_hook: (action -> string -> unit) -> unit
val get_names: unit -> string list
+ val status: unit -> unit
val lookup_theory: string -> theory option
val get_theory: string -> theory
val is_finished: string -> bool
@@ -34,10 +35,11 @@
datatype action = Update | Remove;
local
- val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
+ val hooks = Synchronized.var "Thy_Info.hooks" ([]: (action -> string -> unit) list);
in
- fun add_hook f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change hooks (cons f));
- fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
+ fun add_hook f = Synchronized.change hooks (cons f);
+ fun perform action name =
+ List.app (fn f => (try (fn () => f action name) (); ())) (Synchronized.value hooks);
end;
@@ -87,6 +89,9 @@
fun get_names () = Graph.topological_order (get_thys ());
+fun status () =
+ List.app (Output.status o Markup.markup_only o Markup.loaded_theory) (get_names ());
+
(* access thy *)
@@ -135,7 +140,7 @@
(** thy operations **)
-(* remove theory *)
+(* main loader actions *)
fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
if is_finished name then error (loader_msg "attempt to change finished theory" [name])
@@ -151,11 +156,23 @@
if known_thy name then remove_thy name
else ());
+fun update_thy deps theory = NAMED_CRITICAL "Thy_Info" (fn () =>
+ let
+ val name = Context.theory_name theory;
+ val parents = map Context.theory_name (Theory.parents_of theory);
+ val _ = kill_thy name;
+ val _ = map get_theory parents;
+ val _ = change_thys (new_entry name parents (SOME deps, SOME theory));
+ val _ = perform Update name;
+ in () end);
+
(* scheduling loader tasks *)
+type result = theory * unit future * (unit -> unit);
+
datatype task =
- Task of string list * (theory list -> (theory * unit future * (unit -> unit))) |
+ Task of string list * (theory list -> result) |
Finished of theory;
fun task_finished (Task _) = false
@@ -163,15 +180,15 @@
local
+fun finish_thy ((thy, present, commit): result) =
+ (Global_Theory.join_proofs thy; Future.join present; commit (); thy);
+
fun schedule_seq task_graph =
((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>
(case Graph.get_node task_graph name of
Task (parents, body) =>
- let
- val (thy, present, commit) = body (map (the o Symtab.lookup tab) parents);
- val _ = Future.join present;
- val _ = commit ();
- in Symtab.update (name, thy) tab end
+ let val result = body (map (the o Symtab.lookup tab) parents)
+ in Symtab.update (name, finish_thy result) tab end
| Finished thy => Symtab.update (name, thy) tab))) |> ignore;
fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
@@ -199,10 +216,8 @@
val _ =
tasks |> maps (fn name =>
let
- val (thy, present, commit) = Future.join (the (Symtab.lookup futures name));
- val _ = Global_Theory.join_proofs thy;
- val _ = Future.join present;
- val _ = commit ();
+ val result = Future.join (the (Symtab.lookup futures name));
+ val _ = finish_thy result;
in [] end handle exn => [Exn.Exn exn])
|> rev |> Exn.release_all;
in () end) ();
@@ -226,7 +241,7 @@
fun required_by _ [] = ""
| required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
-fun load_thy initiators update_time (deps: deps) text name parent_thys =
+fun load_thy initiators update_time deps text name parent_thys =
let
val _ = kill_thy name;
val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
@@ -240,13 +255,7 @@
|> Present.begin_theory update_time dir uses;
val (theory, present) = Outer_Syntax.load_thy name init pos text;
-
- val parents = map Context.theory_name parent_thys;
- fun commit () =
- NAMED_CRITICAL "Thy_Info" (fn () =>
- (map get_theory parents;
- change_thys (new_entry name parents (SOME deps, SOME theory));
- perform Update name));
+ fun commit () = update_thy deps theory;
in (theory, present, commit) end;
fun check_deps dir name =
@@ -274,13 +283,14 @@
let
val path = Path.expand (Path.explode str);
val name = Path.implode (Path.base path);
- val dir' = Path.append dir (Path.dir path);
- val _ = member (op =) initiators name andalso error (cycle_msg initiators);
in
(case try (Graph.get_node tasks) name of
SOME task => (task_finished task, tasks)
| NONE =>
let
+ val dir' = Path.append dir (Path.dir path);
+ val _ = member (op =) initiators name andalso error (cycle_msg initiators);
+
val (current, deps, imports) = check_deps dir' name
handle ERROR msg => cat_error msg
(loader_msg "the error(s) above occurred while examining theory" [name] ^
@@ -332,16 +342,12 @@
let
val name = Context.theory_name theory;
val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
- val parents = map Context.theory_name (Theory.parents_of theory);
val imports = Thy_Load.imports_of theory;
- val deps = make_deps master imports;
in
NAMED_CRITICAL "Thy_Info" (fn () =>
(kill_thy name;
Output.urgent_message ("Registering theory " ^ quote name);
- map get_theory parents;
- change_thys (new_entry name parents (SOME deps, SOME theory));
- perform Update name))
+ update_thy (make_deps master imports) theory))
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_info.scala Wed Jul 06 13:57:52 2011 +0200
@@ -0,0 +1,74 @@
+/* Title: Pure/Thy/thy_info.scala
+ Author: Makarius
+
+Theory and file dependencies.
+*/
+
+package isabelle
+
+
+object Thy_Info
+{
+ /* protocol messages */
+
+ object Loaded_Theory {
+ def unapply(msg: XML.Tree): Option[String] =
+ msg match {
+ case XML.Elem(Markup(Markup.LOADED_THEORY, List((Markup.NAME, name))), _) => Some(name)
+ case _ => None
+ }
+ }
+}
+
+
+class Thy_Info(thy_load: Thy_Load)
+{
+ /* messages */
+
+ private def show_path(names: List[String]): String =
+ names.map(quote).mkString(" via ")
+
+ private def cycle_msg(names: List[String]): String =
+ "Cyclic dependency of " + show_path(names)
+
+ private def required_by(s: String, initiators: List[String]): String =
+ if (initiators.isEmpty) ""
+ else s + "(required by " + show_path(initiators.reverse) + ")"
+
+
+ /* dependencies */
+
+ type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]] // name -> (text, header)
+
+ private def require_thys(ignored: String => Boolean,
+ initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
+ (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
+
+ private def require_thy(ignored: String => Boolean,
+ initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
+ {
+ val path = Path.explode(str)
+ val name = path.base.implode
+
+ if (deps.isDefinedAt(name) || ignored(name)) deps
+ else {
+ val dir1 = dir + path.dir
+ try {
+ if (initiators.contains(name)) error(cycle_msg(initiators))
+ val (text, header) =
+ try { thy_load.check_thy(dir1, name) }
+ catch {
+ case ERROR(msg) =>
+ cat_error(msg, "The error(s) above occurred while examining theory " +
+ quote(name) + required_by("\n", initiators))
+ }
+ require_thys(ignored, name :: initiators, dir1,
+ deps + (name -> Exn.Res(text, header)), header.imports)
+ }
+ catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
+ }
+ }
+
+ def dependencies(dir: Path, str: String): Deps =
+ require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_load.scala Wed Jul 06 13:57:52 2011 +0200
@@ -0,0 +1,15 @@
+/* Title: Pure/Thy/thy_load.scala
+ Author: Makarius
+
+Loading files that contribute to a theory.
+*/
+
+package isabelle
+
+abstract class Thy_Load
+{
+ def is_loaded(name: String): Boolean
+
+ def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
+}
+
--- a/src/Pure/Thy/thy_syntax.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Jul 06 13:57:52 2011 +0200
@@ -99,7 +99,7 @@
/** text edits **/
- def text_edits(session: Session, previous: Document.Version,
+ def text_edits(syntax: Outer_Syntax, previous: Document.Version,
edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
{
/* phase 1: edit individual command source */
@@ -147,7 +147,7 @@
commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
val sources = range.flatMap(_.span.map(_.source))
- val spans0 = parse_spans(session.current_syntax().scan(sources.mkString))
+ val spans0 = parse_spans(syntax.scan(sources.mkString))
val (before_edit, spans1) =
if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
@@ -159,7 +159,7 @@
(Some(last), spans1.take(spans1.length - 1))
else (commands.next(last), spans1)
- val inserted = spans2.map(span => new Command(session.new_id(), span))
+ val inserted = spans2.map(span => new Command(Document.new_id(), span))
val new_commands =
commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
recover_spans(new_commands)
@@ -195,7 +195,7 @@
doc_edits += (name -> Some(cmd_edits))
nodes += (name -> new Document.Node(commands2))
}
- (doc_edits.toList, new Document.Version(session.new_id(), nodes))
+ (doc_edits.toList, new Document.Version(Document.new_id(), nodes))
}
}
}
--- a/src/Pure/build-jars Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/build-jars Wed Jul 06 13:57:52 2011 +0200
@@ -9,6 +9,7 @@
## sources
declare -a SOURCES=(
+ Concurrent/counter.scala
Concurrent/future.scala
Concurrent/simple_thread.scala
Concurrent/volatile.scala
@@ -50,6 +51,8 @@
Thy/completion.scala
Thy/html.scala
Thy/thy_header.scala
+ Thy/thy_info.scala
+ Thy/thy_load.scala
Thy/thy_syntax.scala
library.scala
package.scala
--- a/src/Pure/library.ML Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/library.ML Wed Jul 06 13:57:52 2011 +0200
@@ -28,7 +28,7 @@
val funpow: int -> ('a -> 'a) -> 'a -> 'a
val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
- (*errors*)
+ (*user errors*)
exception ERROR of string
val error: string -> 'a
val cat_error: string -> string -> 'a
@@ -260,7 +260,7 @@
| funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
-(* errors *)
+(* user errors *)
exception ERROR of string;
fun error msg = raise ERROR msg;
--- a/src/Pure/library.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/library.scala Wed Jul 06 13:57:52 2011 +0200
@@ -18,6 +18,27 @@
object Library
{
+ /* user errors */
+
+ object ERROR
+ {
+ def apply(message: String): Throwable = new RuntimeException(message)
+ def unapply(exn: Throwable): Option[String] =
+ exn match {
+ case e: RuntimeException =>
+ val msg = e.getMessage
+ Some(if (msg == null) "" else msg)
+ case _ => None
+ }
+ }
+
+ def error(message: String): Nothing = throw ERROR(message)
+
+ def cat_error(msg1: String, msg2: String): Nothing =
+ if (msg1 == "") error(msg1)
+ else error(msg1 + "\n" + msg2)
+
+
/* lists */
def separate[A](s: A, list: List[A]): List[A] =
@@ -40,6 +61,39 @@
result.toList
}
+ def split_lines(str: String): List[String] = space_explode('\n', str)
+
+
+ /* iterate over chunks (cf. space_explode) */
+
+ def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
+ {
+ private val end = source.length
+ private def next_chunk(i: Int): Option[(CharSequence, Int)] =
+ {
+ if (i < end) {
+ var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
+ Some((source.subSequence(i + 1, j), j))
+ }
+ else None
+ }
+ private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
+
+ def hasNext(): Boolean = state.isDefined
+ def next(): CharSequence =
+ state match {
+ case Some((s, i)) => { state = next_chunk(i); s }
+ case None => Iterator.empty.next()
+ }
+ }
+
+ def first_line(source: CharSequence): String =
+ {
+ val lines = chunks(source)
+ if (lines.hasNext) lines.next.toString
+ else ""
+ }
+
/* strings */
@@ -73,37 +127,6 @@
}
- /* iterate over chunks (cf. space_explode/split_lines in ML) */
-
- def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
- {
- private val end = source.length
- private def next_chunk(i: Int): Option[(CharSequence, Int)] =
- {
- if (i < end) {
- var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
- Some((source.subSequence(i + 1, j), j))
- }
- else None
- }
- private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
-
- def hasNext(): Boolean = state.isDefined
- def next(): CharSequence =
- state match {
- case Some((s, i)) => { state = next_chunk(i); s }
- case None => Iterator.empty.next()
- }
- }
-
- def first_line(source: CharSequence): String =
- {
- val lines = chunks(source)
- if (lines.hasNext) lines.next.toString
- else ""
- }
-
-
/* simple dialogs */
private def simple_dialog(kind: Int, default_title: String)
@@ -160,3 +183,18 @@
Exn.release(result)
}
}
+
+
+class Basic_Library
+{
+ val ERROR = Library.ERROR
+ val error = Library.error _
+ val cat_error = Library.cat_error _
+
+ val space_explode = Library.space_explode _
+ val split_lines = Library.split_lines _
+
+ val quote = Library.quote _
+ val commas = Library.commas _
+ val commas_quote = Library.commas_quote _
+}
--- a/src/Pure/package.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Pure/package.scala Wed Jul 06 13:57:52 2011 +0200
@@ -4,8 +4,7 @@
Toplevel isabelle package.
*/
-package object isabelle
+package object isabelle extends isabelle.Basic_Library
{
- def error(message: String): Nothing = throw new RuntimeException(message)
}
--- a/src/Tools/jEdit/etc/settings Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/etc/settings Wed Jul 06 13:57:52 2011 +0200
@@ -10,7 +10,7 @@
JEDIT_STYLE_SHEETS="$ISABELLE_HOME/etc/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
-ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets"
+ISABELLE_JEDIT_OPTIONS="-m no_brackets -m no_type_brackets"
ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
--- a/src/Tools/jEdit/src/document_model.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Jul 06 13:57:52 2011 +0200
@@ -45,10 +45,10 @@
}
}
- def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
+ def init(session: Session, buffer: Buffer, master_dir: String, thy_name: String): Document_Model =
{
exit(buffer)
- val model = new Document_Model(session, buffer, thy_name)
+ val model = new Document_Model(session, buffer, master_dir, thy_name)
buffer.setProperty(key, model)
model.activate()
model
@@ -56,31 +56,36 @@
}
-class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
+class Document_Model(val session: Session,
+ val buffer: Buffer, val master_dir: String, val thy_name: String)
{
/* pending text edits */
- object pending_edits // owned by Swing thread
+ private def capture_header(): Exn.Result[Thy_Header.Header] =
+ Exn.capture {
+ Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength))
+ }
+
+ private object pending_edits // owned by Swing thread
{
private val pending = new mutable.ListBuffer[Text.Edit]
def snapshot(): List[Text.Edit] = pending.toList
- def flush(more_edits: Option[List[Text.Edit]]*)
+ def flush()
{
Swing_Thread.require()
- val edits = snapshot()
- pending.clear
-
- val all_edits =
- if (edits.isEmpty) more_edits.toList
- else Some(edits) :: more_edits.toList
- if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _)))
+ snapshot() match {
+ case Nil =>
+ case edits =>
+ pending.clear
+ session.edit_node(master_dir + "/" + thy_name, capture_header(), edits)
+ }
}
def init()
{
- Swing_Thread.require()
- flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer)))))
+ flush()
+ session.init_node(master_dir + "/" + thy_name, capture_header(), Isabelle.buffer_text(buffer))
}
private val delay_flush =
@@ -100,7 +105,7 @@
def snapshot(): Document.Snapshot =
{
Swing_Thread.require()
- session.snapshot(thy_name, pending_edits.snapshot())
+ session.snapshot(master_dir + "/" + thy_name, pending_edits.snapshot())
}
--- a/src/Tools/jEdit/src/document_view.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Wed Jul 06 13:57:52 2011 +0200
@@ -78,7 +78,7 @@
Swing_Thread.require()
if (model.buffer == text_area.getBuffer) body
else {
- Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
+ Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
default
}
}
@@ -143,7 +143,7 @@
private def exit_popup() { html_popup.map(_.hide) }
private val html_panel =
- new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
+ new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
private def html_panel_resize()
--- a/src/Tools/jEdit/src/html_panel.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala Wed Jul 06 13:57:52 2011 +0200
@@ -37,11 +37,7 @@
}
-class HTML_Panel(
- system: Isabelle_System,
- initial_font_family: String,
- initial_font_size: Int)
- extends HtmlPanel
+class HTML_Panel(initial_font_family: String, initial_font_size: Int) extends HtmlPanel
{
/** Lobo setup **/
@@ -96,7 +92,7 @@
<head>
<style media="all" type="text/css">
""" +
- system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
+ Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS")))
private val template_tail =
"""
@@ -168,8 +164,7 @@
current_body.flatMap(div =>
Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
.map(t =>
- XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Markup.MESSAGE))),
- HTML.spans(system.symbols, t, true))))
+ XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Markup.MESSAGE))), HTML.spans(t, true))))
val doc =
builder.parse(
new InputSourceImpl(
--- a/src/Tools/jEdit/src/isabelle_encoding.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala Wed Jul 06 13:57:52 2011 +0200
@@ -34,7 +34,7 @@
private def text_reader(in: InputStream, codec: Codec): Reader =
{
val source = new BufferedSource(in)(codec)
- new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
+ new CharArrayReader(Isabelle_System.symbols.decode(source.mkString).toArray)
}
override def getTextReader(in: InputStream): Reader =
@@ -53,7 +53,7 @@
val buffer = new ByteArrayOutputStream(BUFSIZE) {
override def flush()
{
- val text = Isabelle.system.symbols.encode(toString(Standard_System.charset_name))
+ val text = Isabelle_System.symbols.encode(toString(Standard_System.charset_name))
out.write(text.getBytes(Standard_System.charset))
out.flush()
}
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Wed Jul 06 13:57:52 2011 +0200
@@ -28,7 +28,7 @@
extends AbstractHyperlink(start, end, line, "")
{
override def click(view: View) = {
- Isabelle.system.source_file(Path.explode(def_file)) match {
+ Isabelle_System.source_file(Path.explode(def_file)) match {
case None =>
Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
case Some(file) =>
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Jul 06 13:57:52 2011 +0200
@@ -96,7 +96,7 @@
case Some((word, cs)) =>
val ds =
(if (Isabelle_Encoding.is_active(buffer))
- cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
+ cs.map(Isabelle_System.symbols.decode(_)).sortWith(_ < _)
else cs).filter(_ != word)
if (ds.isEmpty) null
else new SideKickCompletion(
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed Jul 06 13:57:52 2011 +0200
@@ -26,7 +26,7 @@
Swing_Thread.require()
private val html_panel =
- new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
+ new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
{
override val handler: PartialFunction[HTML_Panel.Event, Unit] = {
case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" =>
--- a/src/Tools/jEdit/src/plugin.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Jul 06 13:57:52 2011 +0200
@@ -10,14 +10,14 @@
import isabelle._
import java.lang.System
-import java.io.{FileInputStream, IOException}
+import java.io.{File, FileInputStream, IOException}
import java.awt.Font
import scala.collection.mutable
import scala.swing.ComboBox
import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
- Buffer, EditPane, ServiceManager, View}
+ Buffer, EditPane, MiscUtilities, ServiceManager, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
@@ -36,7 +36,6 @@
/* plugin instance */
var plugin: Plugin = null
- var system: Isabelle_System = null
var session: Session = null
@@ -200,9 +199,9 @@
case Some(model) => Some(model)
case None =>
// FIXME strip protocol prefix of URL
- Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match {
- case Some((dir, thy_name)) =>
- Some(Document_Model.init(session, buffer, dir + "/" + thy_name))
+ Thy_Header.split_thy_path(Isabelle_System.posix_path(buffer.getPath)) match {
+ case Some((master_dir, thy_name)) =>
+ Some(Document_Model.init(session, buffer, master_dir, thy_name))
case None => None
}
}
@@ -274,9 +273,9 @@
def default_logic(): String =
{
- val logic = system.getenv("JEDIT_LOGIC")
+ val logic = Isabelle_System.getenv("JEDIT_LOGIC")
if (logic != "") logic
- else system.getenv_strict("ISABELLE_LOGIC")
+ else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
}
class Logic_Entry(val name: String, val description: String)
@@ -288,7 +287,7 @@
{
val entries =
new Logic_Entry("", "default (" + default_logic() + ")") ::
- system.find_logics().map(name => new Logic_Entry(name, name))
+ Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
val component = new ComboBox(entries)
entries.find(_.name == logic) match {
case None =>
@@ -301,7 +300,7 @@
def start_session()
{
val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
- val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
+ val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
val logic = {
val logic = Property("logic")
if (logic != null && logic != "") logic
@@ -314,15 +313,30 @@
class Plugin extends EBPlugin
{
- /* session management */
+ /* editor file store */
+
+ private val file_store = new Session.File_Store
+ {
+ def read(path: Path): String =
+ {
+ val platform_path = Isabelle_System.platform_path(path)
+ val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
- @volatile private var session_ready = false
+ Isabelle.jedit_buffers().find(buffer =>
+ MiscUtilities.resolveSymlinks(buffer.getPath) == canonical_path) match {
+ case Some(buffer) => Isabelle.buffer_text(buffer)
+ case None => Standard_System.read_file(new File(platform_path))
+ }
+ }
+ }
+
+
+ /* session manager */
private val session_manager = actor {
loop {
react {
case phase: Session.Phase =>
- session_ready = phase == Session.Ready
phase match {
case Session.Failed =>
Swing_Thread.now {
@@ -335,7 +349,6 @@
case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
case _ =>
}
-
case bad => System.err.println("session_manager: ignoring bad message " + bad)
}
}
@@ -357,7 +370,7 @@
if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
val buffer = msg.getBuffer
- if (buffer != null && session_ready)
+ if (buffer != null && Isabelle.session.is_ready)
Isabelle.init_model(buffer)
case msg: EditPaneUpdate
@@ -373,7 +386,7 @@
if (buffer != null && text_area != null) {
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
msg.getWhat == EditPaneUpdate.CREATED) {
- if (session_ready)
+ if (Isabelle.session.is_ready)
Isabelle.init_view(buffer, text_area)
}
else Isabelle.exit_view(buffer, text_area)
@@ -391,10 +404,10 @@
{
Isabelle.plugin = this
Isabelle.setup_tooltips()
- Isabelle.system = new Isabelle_System
- Isabelle.system.install_fonts()
- Isabelle.session = new Session(Isabelle.system)
- SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender(Isabelle.system.symbols))
+ Isabelle_System.init()
+ Isabelle_System.install_fonts()
+ Isabelle.session = new Session(file_store)
+ SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
if (ModeProvider.instance.isInstanceOf[ModeProvider])
ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
Isabelle.session.phase_changed += session_manager
--- a/src/Tools/jEdit/src/scala_console.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala Wed Jul 06 13:57:52 2011 +0200
@@ -127,7 +127,7 @@
"The following special toplevel bindings are provided:\n" +
" view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
" console -- jEdit Console plugin instance\n" +
- " Isabelle -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
+ " Isabelle -- Isabelle plugin instance (e.g. Isabelle.session)\n")
}
override def printPrompt(console: Console, out: Output)
--- a/src/Tools/jEdit/src/session_dockable.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Wed Jul 06 13:57:52 2011 +0200
@@ -24,8 +24,8 @@
{
/* main tabs */
- private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14)
- readme.render_document(Isabelle.system.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
+ private val readme = new HTML_Panel("SansSerif", 14)
+ readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
private val syslog = new TextArea(Isabelle.session.syslog())
syslog.editable = false
--- a/src/Tools/jEdit/src/token_markup.scala Wed Jul 06 13:52:42 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Wed Jul 06 13:57:52 2011 +0200
@@ -79,8 +79,9 @@
private def bold_style(style: SyntaxStyle): SyntaxStyle =
font_style(style, _.deriveFont(Font.BOLD))
- class Style_Extender(symbols: Symbol.Interpretation) extends SyntaxUtilities.StyleExtender
+ class Style_Extender extends SyntaxUtilities.StyleExtender
{
+ val symbols = Isabelle_System.symbols
if (symbols.font_names.length > 2)
error("Too many user symbol fonts (max 2 permitted): " + symbols.font_names.mkString(", "))
@@ -105,9 +106,10 @@
}
}
- def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
- : Map[Text.Offset, Byte => Byte] =
+ def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
{
+ val symbols = Isabelle_System.symbols
+
// FIXME symbols.bsub_decoded etc.
def ctrl_style(sym: String): Option[Byte => Byte] =
if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
@@ -122,7 +124,7 @@
}
var offset = 0
var ctrl = ""
- for (sym <- Symbol.iterator_string(text)) {
+ for (sym <- Symbol.iterator(text)) {
if (ctrl_style(sym).isDefined) ctrl = sym
else if (ctrl != "") {
if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {
@@ -163,7 +165,6 @@
{
val context1 =
if (Isabelle.session.is_ready) {
- val symbols = Isabelle.system.symbols
val syntax = Isabelle.session.current_syntax()
val ctxt =
@@ -174,7 +175,7 @@
val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
val context1 = new Line_Context(ctxt1)
- val extended = extended_styles(symbols, line)
+ val extended = extended_styles(line)
var offset = 0
for (token <- tokens) {