--- a/src/HOL/Tools/inductive.ML Fri Nov 30 21:47:44 2012 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Nov 30 22:38:06 2012 +0100
@@ -220,10 +220,12 @@
val {infos, monos, ...} = rep_data ctxt;
val space = Consts.space_of (Proof_Context.consts_of ctxt);
in
- [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, infos))),
+ [Pretty.block
+ (Pretty.breaks
+ (Pretty.str "(co)inductives:" ::
+ map (Pretty.mark_str o #1) (Name_Space.extern_table ctxt (space, infos)))),
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
- |> Pretty.chunks |> Pretty.writeln
- end;
+ end |> Pretty.chunks |> Pretty.writeln;
(* inductive info *)
--- a/src/Pure/General/name_space.ML Fri Nov 30 21:47:44 2012 +0100
+++ b/src/Pure/General/name_space.ML Fri Nov 30 22:38:06 2012 +0100
@@ -63,7 +63,7 @@
val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
'a table * 'a table -> 'a table
val dest_table: Proof.context -> 'a table -> (string * 'a) list
- val extern_table: Proof.context -> 'a table -> (xstring * 'a) list
+ val extern_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
end;
structure Name_Space: NAME_SPACE =
@@ -450,8 +450,10 @@
Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []
|> Library.sort_wrt (#2 o #1);
-fun dest_table ctxt tab = map (apfst #1) (ext_table ctxt tab);
-fun extern_table ctxt tab = map (apfst #2) (ext_table ctxt tab);
+fun dest_table ctxt table = map (apfst #1) (ext_table ctxt table);
+
+fun extern_table ctxt (space, tab) =
+ map (fn ((name, xname), x) => ((markup space name, xname), x)) (ext_table ctxt (space, tab));
end;
--- a/src/Pure/Isar/attrib.ML Fri Nov 30 21:47:44 2012 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Nov 30 22:38:06 2012 +0100
@@ -91,9 +91,10 @@
let
val ctxt = Proof_Context.init_global thy;
val attribs = Attributes.get thy;
- fun prt_attr (name, (_, "")) = Pretty.str name
+ fun prt_attr (name, (_, "")) = Pretty.mark_str name
| prt_attr (name, (_, comment)) =
- Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
+ Pretty.block
+ (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
in
[Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))]
|> Pretty.chunks |> Pretty.writeln
@@ -440,8 +441,8 @@
val thy = Proof_Context.theory_of ctxt;
fun prt (name, config) =
let val value = Config.get ctxt config in
- Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
- Pretty.str (Config.print_value value)]
+ Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
+ Pretty.brk 1, Pretty.str (Config.print_value value)]
end;
val configs = Name_Space.extern_table ctxt (#1 (Attributes.get thy), Configs.get thy);
in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
--- a/src/Pure/Isar/bundle.ML Fri Nov 30 21:47:44 2012 +0100
+++ b/src/Pure/Isar/bundle.ML Fri Nov 30 22:38:06 2012 +0100
@@ -138,7 +138,7 @@
(Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
fun prt_bundle (name, bundle) =
- Pretty.block (Pretty.command "bundle" :: Pretty.str " " :: Pretty.str name ::
+ Pretty.block (Pretty.command "bundle" :: Pretty.str " " :: Pretty.mark_str name ::
Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
in
map prt_bundle (Name_Space.extern_table ctxt (get_bundles ctxt))
--- a/src/Pure/Isar/locale.ML Fri Nov 30 21:47:44 2012 +0100
+++ b/src/Pure/Isar/locale.ML Fri Nov 30 22:38:06 2012 +0100
@@ -608,8 +608,11 @@
(*** diagnostic commands and interfaces ***)
fun print_locales thy =
- Pretty.strs ("locales:" ::
- map #1 (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy)))
+ Pretty.block
+ (Pretty.breaks
+ (Pretty.str "locales:" ::
+ map (Pretty.mark_str o #1)
+ (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy))))
|> Pretty.writeln;
fun pretty_locale thy show_facts name =
--- a/src/Pure/Isar/method.ML Fri Nov 30 21:47:44 2012 +0100
+++ b/src/Pure/Isar/method.ML Fri Nov 30 22:38:06 2012 +0100
@@ -316,9 +316,10 @@
let
val ctxt = Proof_Context.init_global thy;
val meths = Methods.get thy;
- fun prt_meth (name, (_, "")) = Pretty.str name
+ fun prt_meth (name, (_, "")) = Pretty.mark_str name
| prt_meth (name, (_, comment)) =
- Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
+ Pretty.block
+ (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
in
[Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table ctxt meths))]
|> Pretty.chunks |> Pretty.writeln
--- a/src/Pure/Thy/thy_output.ML Fri Nov 30 21:47:44 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML Fri Nov 30 22:38:06 2012 +0100
@@ -127,8 +127,8 @@
val command_names = map #1 (Name_Space.extern_table ctxt commands);
val option_names = map #1 (Name_Space.extern_table ctxt options);
in
- [Pretty.big_list "document antiquotations:" (map Pretty.str command_names),
- Pretty.big_list "document antiquotation options:" (map Pretty.str option_names)]
+ [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
+ Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
|> Pretty.chunks |> Pretty.writeln
end;
--- a/src/Pure/display.ML Fri Nov 30 21:47:44 2012 +0100
+++ b/src/Pure/display.ML Fri Nov 30 22:38:06 2012 +0100
@@ -117,7 +117,7 @@
val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
val prt_term_no_vars = prt_term o Logic.unvarify_global;
- fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
+ fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
val prt_const' = Defs.pretty_const ctxt;
fun pretty_classrel (c, []) = prt_cls c
@@ -145,7 +145,8 @@
fun pretty_abbrev (c, (ty, t)) = Pretty.block
(prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]);
- fun pretty_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term_no_vars t];
+ fun pretty_axm (a, t) =
+ Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
fun pretty_finals reds = Pretty.block
(Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o fst) reds));
@@ -202,7 +203,8 @@
Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
Pretty.big_list "axioms:" (map pretty_axm axms),
- Pretty.strs ("oracles:" :: Thm.extern_oracles ctxt),
+ Pretty.block
+ (Pretty.breaks (Pretty.str "oracles:" :: map Pretty.mark_str (Thm.extern_oracles ctxt))),
Pretty.big_list "definitions:"
[pretty_finals reds0,
Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
--- a/src/Pure/thm.ML Fri Nov 30 21:47:44 2012 +0100
+++ b/src/Pure/thm.ML Fri Nov 30 22:38:06 2012 +0100
@@ -147,7 +147,7 @@
val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
- val extern_oracles: Proof.context -> xstring list
+ val extern_oracles: Proof.context -> (Markup.T * xstring) list
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;