tuned;
authorwenzelm
Wed May 18 11:30:59 2005 +0200 (2005-05-18)
changeset 16002e0557c452138
parent 16001 554836ed1f1b
child 16003 48ae07a95c70
tuned;
src/Pure/General/file.ML
src/Pure/General/name_space.ML
src/Pure/General/scan.ML
src/Pure/General/seq.ML
src/Pure/General/symbol.ML
src/Pure/General/table.ML
src/Pure/Isar/isar_output.ML
     1.1 --- a/src/Pure/General/file.ML	Wed May 18 11:30:58 2005 +0200
     1.2 +++ b/src/Pure/General/file.ML	Wed May 18 11:30:59 2005 +0200
     1.3 @@ -96,7 +96,7 @@
     1.4      | s => SOME (Info s))
     1.5    end;
     1.6  
     1.7 -val exists = isSome o info;
     1.8 +val exists = is_some o info;
     1.9  
    1.10  
    1.11  (* directories *)
     2.1 --- a/src/Pure/General/name_space.ML	Wed May 18 11:30:58 2005 +0200
     2.2 +++ b/src/Pure/General/name_space.ML	Wed May 18 11:30:59 2005 +0200
     2.3 @@ -76,7 +76,7 @@
     2.4  (* basic operations *)
     2.5  
     2.6  fun map_space f xname tab =
     2.7 -  Symtab.update ((xname, f (getOpt (Symtab.lookup (tab, xname), ([], [])))), tab);
     2.8 +  Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab);
     2.9  
    2.10  fun change f xname (name, tab) =
    2.11    map_space (fn (names, names') => (f names name, names')) xname tab;
     3.1 --- a/src/Pure/General/scan.ML	Wed May 18 11:30:58 2005 +0200
     3.2 +++ b/src/Pure/General/scan.ML	Wed May 18 11:30:59 2005 +0200
     3.3 @@ -274,7 +274,7 @@
     3.4  
     3.5  fun drain def_prmpt get stopper scan ((state, xs), src) =
     3.6    (scan (state, xs), src) handle MORE prmpt =>
     3.7 -    (case get (getOpt (prmpt, def_prmpt)) src of
     3.8 +    (case get (if_none prmpt def_prmpt) src of
     3.9        ([], _) => (finite' stopper scan (state, xs), src)
    3.10      | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
    3.11  
    3.12 @@ -284,7 +284,7 @@
    3.13  
    3.14      fun drain_loop recover inp =
    3.15        drain_with (catch scanner) inp handle FAIL msg =>
    3.16 -        (error_msg (getOpt (msg, "Syntax error.")); drain_with recover inp);
    3.17 +        (error_msg (if_none msg "Syntax error."); drain_with recover inp);
    3.18  
    3.19      val ((ys, (state', xs')), src') =
    3.20        (case (get def_prmpt src, opt_recover) of
     4.1 --- a/src/Pure/General/seq.ML	Wed May 18 11:30:58 2005 +0200
     4.2 +++ b/src/Pure/General/seq.ML	Wed May 18 11:30:59 2005 +0200
     4.3 @@ -71,8 +71,8 @@
     4.4  fun single x = cons (x, empty);
     4.5  
     4.6  (*head and tail -- beware of calling the sequence function twice!!*)
     4.7 -fun hd xq = #1 (valOf (pull xq))
     4.8 -and tl xq = #2 (valOf (pull xq));
     4.9 +fun hd xq = #1 (the (pull xq))
    4.10 +and tl xq = #2 (the (pull xq));
    4.11  
    4.12  (*partial function as procedure*)
    4.13  fun try f x =
     5.1 --- a/src/Pure/General/symbol.ML	Wed May 18 11:30:58 2005 +0200
     5.2 +++ b/src/Pure/General/symbol.ML	Wed May 18 11:30:59 2005 +0200
     5.3 @@ -342,7 +342,7 @@
     5.4      else if is_ascii_quasi s then Quasi
     5.5      else if is_ascii_blank s then Blank
     5.6      else if is_char s then Other
     5.7 -    else getOpt (Symtab.lookup (symbol_kinds, s), Other);
     5.8 +    else if_none (Symtab.lookup (symbol_kinds, s)) Other;
     5.9  end;
    5.10  
    5.11  fun is_letter s = kind s = Letter;
    5.12 @@ -417,7 +417,7 @@
    5.13  fun sym_explode str =
    5.14    let val chs = explode str in
    5.15      if no_explode chs then chs
    5.16 -    else valOf (Scan.read stopper (Scan.repeat scan) chs)
    5.17 +    else the (Scan.read stopper (Scan.repeat scan) chs)
    5.18    end;
    5.19  
    5.20  val chars_only = not o exists_string (equal "\\");
     6.1 --- a/src/Pure/General/table.ML	Wed May 18 11:30:58 2005 +0200
     6.2 +++ b/src/Pure/General/table.ML	Wed May 18 11:30:59 2005 +0200
     6.3 @@ -95,12 +95,12 @@
     6.4  fun exists P tab = foldl_table (fn (false, e) => P e | (b, _) => b) (false, tab);
     6.5  
     6.6  fun min_key Empty = NONE
     6.7 -  | min_key (Branch2 (left, (k, _), _)) = SOME (getOpt (min_key left, k))
     6.8 -  | min_key (Branch3 (left, (k, _), _, _, _)) = SOME (getOpt (min_key left, k));
     6.9 +  | min_key (Branch2 (left, (k, _), _)) = SOME (if_none (min_key left) k)
    6.10 +  | min_key (Branch3 (left, (k, _), _, _, _)) = SOME (if_none (min_key left) k);
    6.11  
    6.12  fun max_key Empty = NONE
    6.13 -  | max_key (Branch2 (_, (k, _), right)) = SOME (getOpt (max_key right, k))
    6.14 -  | max_key (Branch3 (_, _, _, (k,_), right)) = SOME (getOpt (max_key right, k));
    6.15 +  | max_key (Branch2 (_, (k, _), right)) = SOME (if_none (max_key right) k)
    6.16 +  | max_key (Branch3 (_, _, _, (k,_), right)) = SOME (if_none (max_key right) k);
    6.17  
    6.18  
    6.19  (* lookup *)
    6.20 @@ -184,7 +184,7 @@
    6.21  fun extend (table, args) =
    6.22    let
    6.23      fun add (key, x) (tab, dups) =
    6.24 -      if isSome (lookup (tab, key)) then (tab, key :: dups)
    6.25 +      if is_some (lookup (tab, key)) then (tab, key :: dups)
    6.26        else (update ((key, x), tab), dups);
    6.27    in
    6.28      (case fold add args (table, []) of
    6.29 @@ -212,12 +212,12 @@
    6.30    | del NONE (Branch3 (Empty, p, Empty, q, Empty)) =
    6.31        (p, (false, Branch2 (Empty, q, Empty)))
    6.32    | del k (Branch2 (Empty, p, Empty)) = (case compare k p of
    6.33 -      EQUAL => (p, (true, Empty)) | _ => raise UNDEF (valOf k))
    6.34 +      EQUAL => (p, (true, Empty)) | _ => raise UNDEF (the k))
    6.35    | del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare k p of
    6.36        EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
    6.37      | _ => (case compare k q of
    6.38          EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
    6.39 -      | _ => raise UNDEF (valOf k)))
    6.40 +      | _ => raise UNDEF (the k)))
    6.41    | del k (Branch2 (l, p, r)) = (case compare k p of
    6.42        LESS => (case del k l of
    6.43          (p', (false, l')) => (p', (false, Branch2 (l', p, r)))
    6.44 @@ -311,7 +311,7 @@
    6.45  
    6.46  (* tables with multiple entries per key *)
    6.47  
    6.48 -fun lookup_multi arg = getOpt (lookup arg, []);
    6.49 +fun lookup_multi arg = if_none (lookup arg) [];
    6.50  
    6.51  fun update_multi ((key, x), tab) = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;
    6.52  
     7.1 --- a/src/Pure/Isar/isar_output.ML	Wed May 18 11:30:58 2005 +0200
     7.2 +++ b/src/Pure/Isar/isar_output.ML	Wed May 18 11:30:59 2005 +0200
     7.3 @@ -1,6 +1,6 @@
     7.4  (*  Title:      Pure/Isar/isar_output.ML
     7.5      ID:         $Id$
     7.6 -    Author:     Florian Haftmann, TU Muenchen
     7.7 +    Author:     Markus Wenzel, TU Muenchen
     7.8  
     7.9  Isar theory output.
    7.10  *)
    7.11 @@ -310,6 +310,7 @@
    7.12    ("source", Library.setmp source o boolean),
    7.13    ("goals_limit", Library.setmp goals_limit o integer)];
    7.14  
    7.15 +
    7.16  (* commands *)
    7.17  
    7.18  fun cond_quote prt =
    7.19 @@ -345,23 +346,17 @@
    7.20  
    7.21  fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
    7.22  
    7.23 -fun pretty_term_typ_old ctxt term = Pretty.block [
    7.24 -  ((ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt) term),
    7.25 -  (Pretty.str "\\<Colon>") (* q'n'd *),
    7.26 -  ((ProofContext.pretty_typ ctxt o Term.type_of o ProofContext.extern_skolem ctxt) term)
    7.27 -  ]
    7.28 +fun pretty_term_typ ctxt t =
    7.29 +  (Syntax.const Syntax.constrainC $
    7.30 +    ProofContext.extern_skolem ctxt t $
    7.31 +    Syntax.term_of_typ (! show_sorts) (Term.fastype_of t))
    7.32 +  |> ProofContext.pretty_term ctxt;
    7.33  
    7.34 -fun pretty_term_typ ctxt term = let val t = (ProofContext.extern_skolem ctxt term) in
    7.35 -  ProofContext.pretty_term ctxt (
    7.36 -    Syntax.const Syntax.constrainC $ t $ Syntax.term_of_typ (!show_sorts) (fastype_of t)
    7.37 -  )
    7.38 -end;
    7.39 +fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;
    7.40  
    7.41 -fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of o ProofContext.extern_skolem ctxt;
    7.42 -
    7.43 -fun pretty_term_const ctxt (Const c) = pretty_term ctxt (Const c)
    7.44 -  | pretty_term_const ctxt term =
    7.45 -      raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term)))
    7.46 +fun pretty_term_const ctxt t =
    7.47 +  if Term.is_Const t then pretty_term ctxt t
    7.48 +  else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t);
    7.49  
    7.50  fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of;
    7.51