# HG changeset patch
# User bulwahn
# Date 1309953472 -7200
# Node ID 2882832b8d890251b84d8a1270c4514dbde26ba4
# Parent  ff935aea9557aa9f83b87d8242017b6ff20caea9# Parent  bc7d63c7fd6f27a98b9decd9b3912286ff070b0d
merged

diff -r bc7d63c7fd6f -r 2882832b8d89 src/HOL/ATP.thy
--- 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 *}
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/HOL/Probability/Infinite_Product_Measure.thy
--- 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)
diff -r bc7d63c7fd6f -r 2882832b8d89 src/HOL/Probability/Probability_Measure.thy
--- 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)"])
diff -r bc7d63c7fd6f -r 2882832b8d89 src/HOL/SetInterval.thy
--- 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:
diff -r bc7d63c7fd6f -r 2882832b8d89 src/HOL/Tools/ATP/atp_problem.ML
--- 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
diff -r bc7d63c7fd6f -r 2882832b8d89 src/HOL/Tools/ATP/atp_proof.ML
--- 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
diff -r bc7d63c7fd6f -r 2882832b8d89 src/HOL/Tools/ATP/atp_reconstruct.ML
--- 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
diff -r bc7d63c7fd6f -r 2882832b8d89 src/HOL/Tools/ATP/atp_translate.ML
--- 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
diff -r bc7d63c7fd6f -r 2882832b8d89 src/HOL/Tools/Quotient/quotient_def.ML
--- 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 *)
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/Concurrent/counter.scala
--- /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
+  }
+}
+
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/Concurrent/future.ML
--- 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;
 
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/General/markup.ML
--- 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;
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/General/markup.scala
--- 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"
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/General/path.scala
--- 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)
       }
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/General/symbol.scala
--- 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 */
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/General/yxml.scala
--- 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) }
   }
 }
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/Isar/toplevel.ML
--- 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) ();
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/PIDE/command.scala
--- 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 =
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/PIDE/document.ML
--- 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);
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/PIDE/document.scala
--- 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])
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/PIDE/isar_document.ML
--- 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));
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/PIDE/text.scala
--- 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 }
   }
 
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/System/cygwin.scala
--- 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,
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/System/gui_setup.scala
--- 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)
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/System/isabelle_process.ML
--- 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));
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/System/isabelle_process.scala
--- 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))
         //}}}
       }
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/System/isabelle_system.scala
--- 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)))
   }
 }
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/System/session.scala
--- 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)
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/System/session_manager.scala
--- 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
   }
 }
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/System/standard_system.scala
--- 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
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/Thy/html.scala
--- 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 ""
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/Thy/thy_header.scala
--- 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
+  }
 }
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/Thy/thy_info.ML
--- 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;
 
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/Thy/thy_info.scala
--- /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)
+}
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/Thy/thy_load.scala
--- /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)
+}
+
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/Thy/thy_syntax.scala
--- 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))
     }
   }
 }
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/build-jars
--- 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
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/library.ML
--- 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;
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/library.scala
--- 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 _
+}
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Pure/package.scala
--- 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)
 }
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/etc/settings
--- 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"
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/src/document_model.scala
--- 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())
   }
 
 
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/src/document_view.scala
--- 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()
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/src/html_panel.scala
--- 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(
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/src/isabelle_encoding.scala
--- 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()
       }
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/src/isabelle_hyperlinks.scala
--- 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) =>
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/src/isabelle_sidekick.scala
--- 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(
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/src/output_dockable.scala
--- 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" =>
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/src/plugin.scala
--- 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
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/src/scala_console.scala
--- 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)
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/src/session_dockable.scala
--- 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
diff -r bc7d63c7fd6f -r 2882832b8d89 src/Tools/jEdit/src/token_markup.scala
--- 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) {