tuned;
authorwenzelm
Mon Jun 20 22:14:04 2005 +0200 (2005-06-20)
changeset 16490e10b0d5fa33a
parent 16489 f66ab8a4e98f
child 16491 7310d0a36599
tuned;
src/Pure/Isar/proof_history.ML
src/Pure/Isar/toplevel.ML
src/Pure/display.ML
     1.1 --- a/src/Pure/Isar/proof_history.ML	Mon Jun 20 22:14:03 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof_history.ML	Mon Jun 20 22:14:04 2005 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Histories of proof states, with undo / redo and prev / back.
     1.8 +Histories of proof states, with undo / redo and backtracking.
     1.9  *)
    1.10  
    1.11  signature PROOF_HISTORY =
    1.12 @@ -28,8 +28,8 @@
    1.13  (* datatype proof history *)
    1.14  
    1.15  type node =
    1.16 -  Proof.state *			(*first result*)
    1.17 -  Proof.state Seq.seq; 		(*alternative results*)
    1.18 +  Proof.state *                 (*first result*)
    1.19 +  Proof.state Seq.seq;          (*alternative results*)
    1.20  
    1.21  type proof = node * node list;
    1.22  
    1.23 @@ -55,15 +55,15 @@
    1.24  
    1.25  (* backtrack *)
    1.26  
    1.27 -fun back_fun recur ((_, stq), nodes) =
    1.28 +fun backtrack recur ((_, stq), nodes) =
    1.29    (case Seq.pull stq of
    1.30      NONE =>
    1.31        if recur andalso not (null nodes) then
    1.32 -        (writeln "back: trying previous proof state ..."; back_fun recur (hd nodes, tl nodes))
    1.33 +        (writeln "back: trying previous proof state ..."; backtrack recur (hd nodes, tl nodes))
    1.34        else raise FAIL "back: no alternatives"
    1.35    | SOME result => (result, nodes));
    1.36  
    1.37 -val back = hist_app o back_fun;
    1.38 +val back = hist_app o backtrack;
    1.39  
    1.40  
    1.41  (* apply transformer *)
     2.1 --- a/src/Pure/Isar/toplevel.ML	Mon Jun 20 22:14:03 2005 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jun 20 22:14:04 2005 +0200
     2.3 @@ -7,8 +7,7 @@
     2.4  
     2.5  signature TOPLEVEL =
     2.6  sig
     2.7 -  datatype node = Theory of theory | Proof of ProofHistory.T
     2.8 -    | SkipProof of int History.T * theory
     2.9 +  datatype node = Theory of theory | Proof of ProofHistory.T | SkipProof of int History.T * theory
    2.10    type state
    2.11    val toplevel: state
    2.12    val is_toplevel: state -> bool
    2.13 @@ -228,8 +227,7 @@
    2.14        end;
    2.15  
    2.16  fun check_stale state =
    2.17 -  if not (is_stale state) then ()
    2.18 -  else warning "Stale theory encountered!";
    2.19 +  conditional (is_stale state) (fn () => warning "Stale theory encountered!");
    2.20  
    2.21  end;
    2.22  
     3.1 --- a/src/Pure/display.ML	Mon Jun 20 22:14:03 2005 +0200
     3.2 +++ b/src/Pure/display.ML	Mon Jun 20 22:14:04 2005 +0200
     3.3 @@ -261,7 +261,7 @@
     3.4    | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
     3.5    | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
     3.6  
     3.7 -fun sort_idxs vs = map (apsnd (sort (prod_ord String.compare Int.compare))) vs;
     3.8 +fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
     3.9  fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    3.10  
    3.11  fun consts_of t = sort_cnsts (add_consts (t, []));