# HG changeset patch
# User haftmann
# Date 1231228212 -3600
# Node ID c1f024b4d76d4297690e0be6c585f75f110a34aa
# Parent  aa8689d93135f224da51b31bbb1603282009ce8d# Parent  f9ded2d789b93a46a08ee7b63a44f78e469e6584
merged

diff -r f9ded2d789b9 -r c1f024b4d76d src/HOL/Integration.thy
--- a/src/HOL/Integration.thy	Tue Jan 06 08:50:02 2009 +0100
+++ b/src/HOL/Integration.thy	Tue Jan 06 08:50:12 2009 +0100
@@ -6,7 +6,7 @@
 header{*Theory of Integration*}
 
 theory Integration
-imports MacLaurin
+imports Deriv
 begin
 
 text{*We follow John Harrison in formalizing the Gauge integral.*}
@@ -55,14 +55,37 @@
                                          \<bar>rsum(D,p) f - k\<bar> < e)))"
 
 
+lemma psize_unique:
+  assumes 1: "\<forall>n < N. D(n) < D(Suc n)"
+  assumes 2: "\<forall>n \<ge> N. D(n) = D(N)"
+  shows "psize D = N"
+unfolding psize_def
+proof (rule some_equality)
+  show "(\<forall>n<N. D(n) < D(Suc n)) \<and> (\<forall>n\<ge>N. D(n) = D(N))" using prems ..
+next
+  fix M assume "(\<forall>n<M. D(n) < D(Suc n)) \<and> (\<forall>n\<ge>M. D(n) = D(M))"
+  hence 3: "\<forall>n<M. D(n) < D(Suc n)" and 4: "\<forall>n\<ge>M. D(n) = D(M)" by fast+
+  show "M = N"
+  proof (rule linorder_cases)
+    assume "M < N"
+    hence "D(M) < D(Suc M)" by (rule 1 [rule_format])
+    also have "D(Suc M) = D(M)" by (rule 4 [rule_format], simp)
+    finally show "M = N" by simp
+  next
+    assume "N < M"
+    hence "D(N) < D(Suc N)" by (rule 3 [rule_format])
+    also have "D(Suc N) = D(N)" by (rule 2 [rule_format], simp)
+    finally show "M = N" by simp
+  next
+    assume "M = N" thus "M = N" .
+  qed
+qed
+
 lemma partition_zero [simp]: "a = b ==> psize (%n. if n = 0 then a else b) = 0"
-by (auto simp add: psize_def)
+by (rule psize_unique, simp_all)
 
 lemma partition_one [simp]: "a < b ==> psize (%n. if n = 0 then a else b) = 1"
-apply (simp add: psize_def)
-apply (rule some_equality, auto)
-apply (drule_tac x = 1 in spec, auto)
-done
+by (rule psize_unique, simp_all)
 
 lemma partition_single [simp]:
      "a \<le> b ==> partition(a,b)(%n. if n = 0 then a else b)"
@@ -76,20 +99,11 @@
         ((D 0 = a) &
          (\<forall>n < psize D. D n < D(Suc n)) &
          (\<forall>n \<ge> psize D. D n = b))"
-apply (simp add: partition_def, auto)
-apply (subgoal_tac [!] "psize D = N", auto)
-apply (simp_all (no_asm) add: psize_def)
-apply (rule_tac [!] some_equality, blast)
-  prefer 2 apply blast
-apply (rule_tac [!] ccontr)
-apply (simp_all add: linorder_neq_iff, safe)
-apply (drule_tac x = Na in spec)
-apply (rotate_tac 3)
-apply (drule_tac x = "Suc Na" in spec, simp)
-apply (rotate_tac 2)
-apply (drule_tac x = N in spec, simp)
-apply (drule_tac x = Na in spec)
-apply (drule_tac x = "Suc Na" and P = "%n. Na\<le>n \<longrightarrow> D n = D Na" in spec, auto)
+apply (simp add: partition_def)
+apply (rule iffI, clarify)
+apply (subgoal_tac "psize D = N", simp)
+apply (rule psize_unique, assumption, simp)
+apply (simp, rule_tac x="psize D" in exI, simp)
 done
 
 lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)"
@@ -211,26 +225,10 @@
 lemma lemma_partition_append2:
      "[| partition (a, b) D1; partition (b, c) D2 |]
       ==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) =
-          psize D1 + psize D2" 
-apply (unfold psize_def 
-         [of "%n. if n < psize D1 then D1 n else D2 (n - psize D1)"])
-apply (rule some1_equality)
- prefer 2 apply (blast intro!: lemma_partition_append1)
-apply (rule ex1I, rule lemma_partition_append1) 
-apply (simp_all split: split_if_asm)
- txt{*The case @{term "N < psize D1"}*} 
- apply (drule_tac x = "psize D1 + psize D2" and P="%n. ?P n & ?Q n" in spec) 
- apply (force dest: lemma_psize1)
-apply (rule order_antisym);
- txt{*The case @{term "psize D1 \<le> N"}: 
-       proving @{term "N \<le> psize D1 + psize D2"}*}
- apply (drule_tac x = "psize D1 + psize D2" in spec)
- apply (simp add: partition_rhs2)
-apply (case_tac "N - psize D1 < psize D2") 
- prefer 2 apply arith
- txt{*Proving @{term "psize D1 + psize D2 \<le> N"}*}
-apply (drule_tac x = "psize D1 + psize D2" and P="%n. N\<le>n --> ?P n" in spec, simp)
-apply (drule_tac a = b and b = c in partition_gt, assumption, simp)
+          psize D1 + psize D2"
+apply (rule psize_unique)
+apply (erule (1) lemma_partition_append1 [THEN conjunct1])
+apply (erule (1) lemma_partition_append1 [THEN conjunct2])
 done
 
 lemma tpart_eq_lhs_rhs: "[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b"
@@ -566,20 +564,12 @@
 lemma lemma_additivity4_psize_eq:
      "[| a \<le> D n; D n < b; partition (a, b) D |]
       ==> psize (%x. if D x < D n then D(x) else D n) = n"
-apply (unfold psize_def)
-apply (frule lemma_additivity1)
-apply (assumption, assumption)
-apply (rule some_equality)
-apply (auto intro: partition_lt_Suc)
-apply (drule_tac n = n in partition_lt_gen, assumption)
-apply (arith, arith)
-apply (cut_tac x = na and y = "psize D" in less_linear)
-apply (auto dest: partition_lt_cancel)
-apply (rule_tac x=N and y=n in linorder_cases)
-apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
-apply (drule_tac n = n in partition_lt_gen, auto)
-apply (drule_tac x = n in spec)
-apply (simp split: split_if_asm)
+apply (frule (2) lemma_additivity1)
+apply (rule psize_unique, auto)
+apply (erule partition_lt_Suc, erule (1) less_trans)
+apply (erule notE)
+apply (erule (1) partition_lt_gen, erule less_imp_le)
+apply (drule (1) partition_lt_cancel, simp)
 done
 
 lemma lemma_psize_left_less_psize:
diff -r f9ded2d789b9 -r c1f024b4d76d src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Jan 06 08:50:02 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Jan 06 08:50:12 2009 +0100
@@ -199,13 +199,13 @@
 fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt)
 
 val by_pat_completeness_simp =
-    Proof.global_terminal_proof
+    Proof.future_terminal_proof
       (Method.Basic (pat_completeness, Position.none),
        SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
 fun termination_by method =
     FundefPackage.setup_termination_proof NONE
-    #> Proof.global_terminal_proof
+    #> Proof.future_terminal_proof
       (Method.Basic (method, Position.none), NONE)
 
 fun mk_catchall fixes arities =
diff -r f9ded2d789b9 -r c1f024b4d76d src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Tue Jan 06 08:50:02 2009 +0100
+++ b/src/HOLCF/HOLCF.thy	Tue Jan 06 08:50:12 2009 +0100
@@ -24,7 +24,7 @@
 declaration {* fn _ =>
   Simplifier.map_ss (fn simpset => simpset addSolver
     (mk_solver' "adm_tac" (fn ss =>
-      adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
+      Adm.adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
 *}
 
 end
diff -r f9ded2d789b9 -r c1f024b4d76d src/HOLCF/Tools/adm_tac.ML
--- a/src/HOLCF/Tools/adm_tac.ML	Tue Jan 06 08:50:02 2009 +0100
+++ b/src/HOLCF/Tools/adm_tac.ML	Tue Jan 06 08:50:12 2009 +0100
@@ -1,18 +1,16 @@
-(*  ID:         $Id$
-    Author:     Stefan Berghofer, TU Muenchen
+(*  Author:     Stefan Berghofer, TU Muenchen
 
 Admissibility tactic.
 
 Checks whether adm_subst theorem is applicable to the current proof
 state:
 
-  [| cont t; adm P |] ==> adm (%x. P (t x))
+  cont t ==> adm P ==> adm (%x. P (t x))
 
 "t" is instantiated with a term of chain-finite type, so that
 adm_chfin can be applied:
 
   adm (P::'a::{chfin,pcpo} => bool)
-
 *)
 
 signature ADM =
@@ -39,21 +37,19 @@
       if i = lev then [[(Bound 0, path)]]
       else []
   | find_subterms (t as (Abs (_, _, t2))) lev path =
-      if List.filter (fn x => x<=lev)
-           (add_loose_bnos (t, 0, [])) = [lev] then
-        [(incr_bv (~lev, 0, t), path)]::
+      if filter (fn x => x <= lev) (add_loose_bnos (t, 0, [])) = [lev]
+      then
+        [(incr_bv (~lev, 0, t), path)] ::
         (find_subterms t2 (lev+1) (0::path))
       else find_subterms t2 (lev+1) (0::path)
   | find_subterms (t as (t1 $ t2)) lev path =
       let val ts1 = find_subterms t1 lev (0::path);
           val ts2 = find_subterms t2 lev (1::path);
           fun combine [] y = []
-            | combine (x::xs) ys =
-                (map (fn z => x @ z) ys) @ (combine xs ys)
+            | combine (x::xs) ys = map (fn z => x @ z) ys @ combine xs ys
       in
-        (if List.filter (fn x => x<=lev)
-              (add_loose_bnos (t, 0, [])) = [lev] then
-           [[(incr_bv (~lev, 0, t), path)]]
+        (if filter (fn x => x <= lev) (add_loose_bnos (t, 0, [])) = [lev]
+         then [[(incr_bv (~lev, 0, t), path)]]
          else []) @
         (if ts1 = [] then ts2
          else if ts2 = [] then ts1
@@ -65,7 +61,7 @@
 (*** make term for instantiation of predicate "P" in adm_subst theorem ***)
 
 fun make_term t path paths lev =
-  if path mem paths then Bound lev
+  if member (op =) paths path then Bound lev
   else case t of
       (Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1))
     | (t1 $ t2) => (make_term t1 (0::path) paths lev) $
@@ -79,30 +75,24 @@
   | eq_terms (ts as (t, _) :: _) = forall (fn (t2, _) => t2 aconv t) ts;
 
 
-(*figure out internal names*)
-val chfin_pcpoS = Sign.intern_sort (the_context ()) ["chfin", "pcpo"];
-val cont_name = Sign.intern_const (the_context ()) "cont";
-val adm_name = Sign.intern_const (the_context ()) "adm";
-
-
 (*** check whether type of terms in list is chain finite ***)
 
-fun is_chfin sign T params ((t, _)::_) =
+fun is_chfin thy T params ((t, _)::_) =
   let val parTs = map snd (rev params)
-  in Sign.of_sort sign (fastype_of1 (T::parTs, t), chfin_pcpoS) end;
+  in Sign.of_sort thy (fastype_of1 (T::parTs, t), @{sort "{chfin,pcpo}"}) end;
 
 
 (*** try to prove that terms in list are continuous
      if successful, add continuity theorem to list l ***)
 
-fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) =
+fun prove_cont tac thy s T prems params (ts as ((t, _)::_)) l =
   let val parTs = map snd (rev params);
        val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
        fun mk_all [] t = t
          | mk_all ((a,T)::Ts) t = Term.all T $ (Abs (a, T, mk_all Ts t));
-       val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
+       val t = HOLogic.mk_Trueprop (Const (@{const_name cont}, contT) $ Abs (s, T, t));
        val t' = mk_all params (Logic.list_implies (prems, t));
-       val thm = Goal.prove (ProofContext.init sign) [] [] t' (K (tac 1));
+       val thm = Goal.prove (ProofContext.init thy) [] [] t' (K (tac 1));
   in (ts, thm)::l end
   handle ERROR _ => l;
 
@@ -111,71 +101,59 @@
 
 fun inst_adm_subst_thm state i params s T subt t paths =
   let
-      val sign = Thm.theory_of_thm state;
-      val j = Thm.maxidx_of state + 1;
-      val parTs = map snd (rev params);
-      val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst};
-      val types = valOf o (fst (Drule.types_sorts rule));
-      val tT = types ("t", j);
-      val PT = types ("P", j);
-      fun mk_abs [] t = t
-        | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
-      val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
-      val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
-                     (make_term t [] paths 0));
-      val tye = Sign.typ_match sign (tT, #T (rep_cterm tt)) Vartab.empty;
-      val tye' = Sign.typ_match sign (PT, #T (rep_cterm Pt)) tye;
-      val ctye = map (fn (ixn, (S, T)) =>
-        (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye');
-      val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT));
-      val Pv = cterm_of sign (Var (("P", j), Envir.typ_subst_TVars tye' PT));
-      val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
+    val thy = Thm.theory_of_thm state;
+    val j = Thm.maxidx_of state + 1;
+    val parTs = map snd (rev params);
+    val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst};
+    val types = the o fst (Drule.types_sorts rule);
+    val tT = types ("t", j);
+    val PT = types ("P", j);
+    fun mk_abs [] t = t
+      | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
+    val tt = cterm_of thy (mk_abs (params @ [(s, T)]) subt);
+    val Pt = cterm_of thy (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
+                   (make_term t [] paths 0));
+    val tye = Sign.typ_match thy (tT, #T (rep_cterm tt)) Vartab.empty;
+    val tye' = Sign.typ_match thy (PT, #T (rep_cterm Pt)) tye;
+    val ctye = map (fn (ixn, (S, T)) =>
+      (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)) (Vartab.dest tye');
+    val tv = cterm_of thy (Var (("t", j), Envir.typ_subst_TVars tye' tT));
+    val Pv = cterm_of thy (Var (("P", j), Envir.typ_subst_TVars tye' PT));
+    val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
   in rule' end;
 
 
-(*** extract subgoal i from proof state ***)
-
-fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
-
-
 (*** the admissibility tactic ***)
 
-fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) =
-      if name = adm_name then SOME abs else NONE
+fun try_dest_adm (Const _ $ (Const (@{const_name adm}, _) $ Abs abs)) = SOME abs
   | try_dest_adm _ = NONE;
 
-fun adm_tac tac i state =
-  state |>
-  let val goali = nth_subgoal i state in
-    (case try_dest_adm (Logic.strip_assums_concl goali) of
-      NONE => no_tac
-    | SOME (s, T, t) =>
-        let
-          val sign = Thm.theory_of_thm state;
-          val prems = Logic.strip_assums_hyp goali;
-          val params = Logic.strip_params goali;
-          val ts = find_subterms t 0 [];
-          val ts' = List.filter eq_terms ts;
-          val ts'' = List.filter (is_chfin sign T params) ts';
-          val thms = Library.foldl (prove_cont tac sign s T prems params) ([], ts'');
-        in
-          (case thms of
-            ((ts as ((t', _)::_), cont_thm)::_) =>
-              let
-                val paths = map snd ts;
-                val rule = inst_adm_subst_thm state i params s T t' t paths;
-              in
-                compose_tac (false, rule, 2) i THEN
-                rtac cont_thm i THEN
-                REPEAT (assume_tac i) THEN
-                rtac @{thm adm_chfin} i
-              end 
-          | [] => no_tac)
-        end)
-    end;
-
+fun adm_tac tac i state = (i, state) |-> SUBGOAL (fn (goali, _) =>
+  (case try_dest_adm (Logic.strip_assums_concl goali) of
+    NONE => no_tac
+  | SOME (s, T, t) =>
+      let
+        val thy = Thm.theory_of_thm state;
+        val prems = Logic.strip_assums_hyp goali;
+        val params = Logic.strip_params goali;
+        val ts = find_subterms t 0 [];
+        val ts' = filter eq_terms ts;
+        val ts'' = filter (is_chfin thy T params) ts';
+        val thms = fold (prove_cont tac thy s T prems params) ts'' [];
+      in
+        (case thms of
+          ((ts as ((t', _)::_), cont_thm) :: _) =>
+            let
+              val paths = map snd ts;
+              val rule = inst_adm_subst_thm state i params s T t' t paths;
+            in
+              compose_tac (false, rule, 2) i THEN
+              resolve_tac [cont_thm] i THEN
+              REPEAT (assume_tac i) THEN
+              resolve_tac [@{thm adm_chfin}] i
+            end
+        | [] => no_tac)
+      end));
 
 end;
 
-
-open Adm;
diff -r f9ded2d789b9 -r c1f024b4d76d src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Tue Jan 06 08:50:02 2009 +0100
+++ b/src/Pure/Isar/isar.ML	Tue Jan 06 08:50:12 2009 +0100
@@ -6,15 +6,12 @@
 
 signature ISAR =
 sig
-  type id = string
-  val no_id: id
-  val create_command: Toplevel.transition -> id
-  val init_point: unit -> unit
+  val init: unit -> unit
+  val exn: unit -> (exn * string) option
   val state: unit -> Toplevel.state
   val context: unit -> Proof.context
   val goal: unit -> thm
   val print: unit -> unit
-  val exn: unit -> (exn * string) option
   val >> : Toplevel.transition -> bool
   val >>> : Toplevel.transition list -> unit
   val linear_undo: int -> unit
@@ -25,6 +22,10 @@
   val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
   val loop: unit -> unit
   val main: unit -> unit
+
+  type id = string
+  val no_id: id
+  val create_command: Toplevel.transition -> id
   val insert_command: id -> id -> unit
   val remove_command: id -> unit
 end;
@@ -33,6 +34,130 @@
 struct
 
 
+(** TTY model -- SINGLE-THREADED! **)
+
+(* the global state *)
+
+type history = (Toplevel.state * Toplevel.transition) list;
+  (*previous state, state transition -- regular commands only*)
+
+local
+  val global_history = ref ([]: history);
+  val global_state = ref Toplevel.toplevel;
+  val global_exn = ref (NONE: (exn * string) option);
+in
+
+fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
+  let
+    fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
+      | edit n (st, hist) = edit (n - 1) (f st hist);
+  in edit count (! global_state, ! global_history) end);
+
+fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
+fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
+
+fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
+fun set_exn exn =  NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
+
+end;
+
+
+fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
+
+fun context () = Toplevel.context_of (state ())
+  handle Toplevel.UNDEF => error "Unknown context";
+
+fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
+  handle Toplevel.UNDEF => error "No goal present";
+
+fun print () = Toplevel.print_state false (state ());
+
+
+(* history navigation *)
+
+local
+
+fun find_and_undo _ [] = error "Undo history exhausted"
+  | find_and_undo which ((prev, tr) :: hist) =
+      ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
+        if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
+
+in
+
+fun linear_undo n = edit_history n (K (find_and_undo (K true)));
+
+fun undo n = edit_history n (fn st => fn hist =>
+  find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
+
+fun kill () = edit_history 1 (fn st => fn hist =>
+  find_and_undo
+    (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
+
+fun kill_proof () = edit_history 1 (fn st => fn hist =>
+  if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
+  else raise Toplevel.UNDEF);
+
+end;
+
+
+(* interactive state transformations *)
+
+fun op >> tr =
+  (case Toplevel.transition true tr (state ()) of
+    NONE => false
+  | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
+  | SOME (st', NONE) =>
+      let
+        val name = Toplevel.name_of tr;
+        val _ = if OuterKeyword.is_theory_begin name then init () else ();
+        val _ =
+          if OuterKeyword.is_regular name
+          then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
+      in true end);
+
+fun op >>> [] = ()
+  | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
+
+
+(* toplevel loop *)
+
+val crashes = ref ([]: exn list);
+
+local
+
+fun raw_loop secure src =
+  let
+    fun check_secure () =
+      (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
+  in
+    (case Source.get_single (Source.set_prompt Source.default_prompt src) of
+      NONE => if secure then quit () else ()
+    | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
+    handle exn => (Output.error_msg (Toplevel.exn_message exn)
+    handle crash =>
+      (CRITICAL (fn () => change crashes (cons crash));
+        warning "Recovering after Isar toplevel crash -- see also Isar.crashes");
+      raw_loop secure src)
+  end;
+
+in
+
+fun toplevel_loop {init = do_init, welcome, sync, secure} =
+ (Context.set_thread_data NONE;
+  if do_init then init () else ();  (* FIXME init editor model *)
+  if welcome then writeln (Session.welcome ()) else ();
+  uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
+
+end;
+
+fun loop () =
+  toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
+
+fun main () =
+  toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
+
+
+
 (** individual toplevel commands **)
 
 (* unique identification *)
@@ -188,153 +313,6 @@
 
 
 
-(** TTY model -- single-threaded **)
-
-(* global point *)
-
-local val global_point = ref no_id in
-
-fun change_point f = NAMED_CRITICAL "Isar" (fn () => change global_point f);
-fun point () = NAMED_CRITICAL "Isar" (fn () => ! global_point);
-
-end;
-
-
-fun set_point id = change_point (K id);
-fun init_point () = set_point no_id;
-
-fun point_state () = NAMED_CRITICAL "Isar" (fn () =>
-  let val id = point () in (id, the_state id) end);
-
-fun state () = #2 (point_state ());
-
-fun context () =
-  Toplevel.context_of (state ())
-    handle Toplevel.UNDEF => error "Unknown context";
-
-fun goal () =
-  #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
-    handle Toplevel.UNDEF => error "No goal present";
-
-fun print () = Toplevel.print_state false (state ());
-
-
-(* global failure status *)
-
-local val global_exn = ref (NONE: (exn * string) option) in
-
-fun set_exn err = global_exn := err;
-fun exn () = ! global_exn;
-
-end;
-
-
-(* interactive state transformations *)
-
-fun op >> raw_tr =
-  let
-    val id = create_command raw_tr;
-    val {category, transition = tr, ...} = the_command id;
-    val (prev, prev_state) = point_state ();
-    val _ =
-      if is_regular category
-      then (dispose_commands (next_commands prev); change_commands (add_edge (prev, id)))
-      else ();
-  in
-    (case run true tr prev_state of
-      NONE => false
-    | SOME (status as Failed err) => (update_status status id; set_exn (SOME err); true)
-    | SOME status =>
-       (update_status status id; set_exn NONE;
-        if is_regular category then set_point id else ();
-        true))
-  end;
-
-fun op >>> [] = ()
-  | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
-
-
-(* implicit navigation wrt. proper commands *)
-
-local
-
-fun err_undo () = error "Undo history exhausted";
-
-fun find_category which id =
-  (case #category (the_command id) of
-    Empty => err_undo ()
-  | category => if which category then id else find_category which (prev_command id));
-
-fun find_begin_theory id =
-  if id = no_id then err_undo ()
-  else if is_some (Toplevel.init_of (#transition (the_command id))) then id
-  else find_begin_theory (prev_command id);
-
-fun undo_command id =
-  (case Toplevel.init_of (#transition (the_command id)) of
-    SOME name => prev_command id before ThyInfo.kill_thy name
-  | NONE => prev_command id);
-
-in
-
-fun linear_undo n = change_point (funpow n (fn id => undo_command (find_category is_proper id)));
-
-fun undo n = change_point (funpow n (fn id => undo_command
-  (find_category (if Toplevel.is_proof (the_state id) then is_proper else is_theory) id)));
-
-fun kill () = change_point (fn id => undo_command
-  (if Toplevel.is_proof (the_state id) then find_category is_theory id else find_begin_theory id));
-
-fun kill_proof () = change_point (fn id =>
-  if Toplevel.is_proof (the_state id) then undo_command (find_category is_theory id)
-  else raise Toplevel.UNDEF);
-
-end;
-
-
-(* toplevel loop *)
-
-val crashes = ref ([]: exn list);
-
-local
-
-fun raw_loop secure src =
-  let
-    fun check_secure () =
-      (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
-    val prev = point ();
-    val prev_name = Toplevel.name_of (#transition (the_command prev));
-    val prompt_markup =
-      prev <> no_id ? Markup.markup
-        (Markup.properties [(Markup.idN, prev), (Markup.nameN, prev_name)] Markup.prompt);
-  in
-    (case Source.get_single (Source.set_prompt (prompt_markup Source.default_prompt) src) of
-      NONE => if secure then quit () else ()
-    | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
-    handle exn => (Output.error_msg (Toplevel.exn_message exn) handle crash =>
-      (CRITICAL (fn () => change crashes (cons crash));
-        warning "Recovering after Isar toplevel crash -- see also Isar.crashes");
-      raw_loop secure src)
-  end;
-
-in
-
-fun toplevel_loop {init, welcome, sync, secure} =
- (Context.set_thread_data NONE;
-  if init then (init_point (); init_commands ()) else ();
-  if welcome then writeln (Session.welcome ()) else ();
-  uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
-
-end;
-
-fun loop () =
-  toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
-
-fun main () =
-  toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
-
-
-
 (** editor model **)
 
 (* run commands *)
@@ -375,7 +353,7 @@
 
 local
 
-structure P = struct open OuterParse open ValueParse end;
+structure P = OuterParse;
 val op >> = Scan.>>;
 
 in
diff -r f9ded2d789b9 -r c1f024b4d76d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jan 06 08:50:02 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jan 06 08:50:12 2009 +0100
@@ -771,7 +771,7 @@
 
 val _ =
   OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init_point));
+    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init));
 
 val _ =
   OuterSyntax.improper_command "linear_undo" "undo commands" K.control
diff -r f9ded2d789b9 -r c1f024b4d76d src/Pure/Isar/locale.ML
diff -r f9ded2d789b9 -r c1f024b4d76d src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Tue Jan 06 08:50:02 2009 +0100
+++ b/src/Pure/Isar/outer_keyword.ML	Tue Jan 06 08:50:12 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/outer_keyword.ML
-    ID:         $Id$
     Author:     Makarius
 
 Isar command keyword classification and global keyword tables.
@@ -47,9 +46,12 @@
   val report: unit -> unit
   val keyword: string -> unit
   val command: string -> T -> unit
+  val is_diag: string -> bool
+  val is_control: string -> bool
+  val is_regular: string -> bool
+  val is_theory_begin: string -> bool
   val is_theory: string -> bool
   val is_proof: string -> bool
-  val is_diag: string -> bool
   val is_theory_goal: string -> bool
   val is_proof_goal: string -> bool
   val is_qed: string -> bool
@@ -174,6 +176,12 @@
     NONE => false
   | SOME k => member (op = o pairself kind_of) ks k);
 
+val is_diag = command_category [diag];
+val is_control = command_category [control];
+fun is_regular name = not (is_diag name orelse is_control name);
+
+val is_theory_begin = command_category [thy_begin];
+
 val is_theory = command_category
   [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal];
 
@@ -181,8 +189,6 @@
   [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
     prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
 
-val is_diag = command_category [diag];
-
 val is_theory_goal = command_category [thy_goal];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal];
 val is_qed = command_category [qed, qed_block];
diff -r f9ded2d789b9 -r c1f024b4d76d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jan 06 08:50:02 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Jan 06 08:50:12 2009 +0100
@@ -115,6 +115,7 @@
     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
   val is_relevant: state -> bool
   val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
+  val future_terminal_proof: Method.text * Method.text option -> state -> context
 end;
 
 structure Proof: PROOF =
@@ -1027,5 +1028,10 @@
 
 end;
 
+fun future_terminal_proof meths state =
+  if is_relevant state then global_terminal_proof meths state
+  else #2 (state |> future_proof (fn state' =>
+    Future.fork_pri ~1 (fn () => ((), global_terminal_proof meths state'))));
+
 end;
 
diff -r f9ded2d789b9 -r c1f024b4d76d src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jan 06 08:50:02 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jan 06 08:50:12 2009 +0100
@@ -144,7 +144,7 @@
             (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
               tell_file_retracted (ThyLoad.thy_path name))
       else ();
-    val _ = Isar.init_point ();
+    val _ = Isar.init ();
   in () end;
 
 
@@ -156,7 +156,7 @@
  (sync_thy_loader ();
   tell_clear_goals ();
   tell_clear_response ();
-  Isar.init_point ();
+  Isar.init ();
   welcome ());
 
 
diff -r f9ded2d789b9 -r c1f024b4d76d src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jan 06 08:50:02 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jan 06 08:50:12 2009 +0100
@@ -242,7 +242,7 @@
     (sync_thy_loader ();
      tell_clear_goals ();
      tell_clear_response ();
-     Isar.init_point ();
+     Isar.init ();
      welcome ());