src/Pure/display.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/display.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/display.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -122,7 +122,7 @@
     1.4    (Seq.print (fn _ => print_thm) 100000 thseq; thseq);
     1.5  
     1.6  (*Print and return a list of theorems, separated by blank lines. *)
     1.7 -fun prths ths = (seq (fn th => (print_thm th; writeln "")) ths; ths);
     1.8 +fun prths ths = (List.app (fn th => (print_thm th; writeln "")) ths; ths);
     1.9  
    1.10  
    1.11  (* other printing commands *)
    1.12 @@ -210,7 +210,7 @@
    1.13            if not syn then NONE
    1.14            else SOME (prt_typ (Type (t, [])));
    1.15  
    1.16 -    val pretty_arities = flat o map (fn (t, ars) => map (prt_arity t) ars);
    1.17 +    val pretty_arities = List.concat o map (fn (t, ars) => map (prt_arity t) ars);
    1.18  
    1.19      fun pretty_const (c, (ty, _)) = Pretty.block
    1.20        [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    1.21 @@ -238,13 +238,13 @@
    1.22    in
    1.23      [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
    1.24        Pretty.strs ("data:" :: Sign.data_kinds data),
    1.25 -      Pretty.strs ["name prefix:", NameSpace.pack (if_none path ["-"])],
    1.26 +      Pretty.strs ["name prefix:", NameSpace.pack (getOpt (path,["-"]))],
    1.27        Pretty.big_list "name spaces:" (map pretty_name_space spcs),
    1.28        Pretty.big_list "classes:" (map pretty_classrel (Graph.dest classes)),
    1.29        pretty_default default,
    1.30        pretty_witness witness,
    1.31 -      Pretty.big_list "syntactic types:" (mapfilter (pretty_type true) tdecls),
    1.32 -      Pretty.big_list "logical types:" (mapfilter (pretty_type false) tdecls),
    1.33 +      Pretty.big_list "syntactic types:" (List.mapPartial (pretty_type true) tdecls),
    1.34 +      Pretty.big_list "logical types:" (List.mapPartial (pretty_type false) tdecls),
    1.35        Pretty.big_list "type arities:" (pretty_arities (Symtab.dest arities)),
    1.36        Pretty.big_list "consts:" (map pretty_const cnsts),
    1.37        Pretty.big_list "finals consts:" (map pretty_final finals),
    1.38 @@ -282,7 +282,7 @@
    1.39    | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
    1.40    | add_vars (_, env) = env;
    1.41  
    1.42 -fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env)
    1.43 +fun add_varsT (Type (_, Ts), env) = Library.foldr add_varsT (Ts, env)
    1.44    | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
    1.45    | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
    1.46  
    1.47 @@ -334,7 +334,7 @@
    1.48        (if main then [Pretty.term pp B] else []) @
    1.49         (if ngoals = 0 then [Pretty.str "No subgoals!"]
    1.50          else if ngoals > maxgoals then
    1.51 -          pretty_subgoals (take (maxgoals, As)) @
    1.52 +          pretty_subgoals (Library.take (maxgoals, As)) @
    1.53            (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
    1.54             else [])
    1.55          else pretty_subgoals As) @