--- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Feb 26 10:53:19 2014 +0100
@@ -247,7 +247,7 @@
map pretty_typ_bracket tys));
val pretty_datatype =
Pretty.block
- (Pretty.command "datatype" :: Pretty.brk 1 ::
+ (Pretty.keyword1 "datatype" :: Pretty.brk 1 ::
Syntax.pretty_typ ctxt ty ::
Pretty.str " =" :: Pretty.brk 1 ::
flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos)));
--- a/src/Pure/General/pretty.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/Pure/General/pretty.ML Wed Feb 26 10:53:19 2014 +0100
@@ -40,8 +40,9 @@
val marks_str: Markup.T list * string -> T
val item: T list -> T
val text_fold: T list -> T
- val command: string -> T
- val keyword: string -> T
+ val keyword1: string -> T
+ val keyword2: string -> T
+ val keyword3: string -> T
val text: string -> T list
val paragraph: T list -> T
val para: string -> T
@@ -163,8 +164,9 @@
val item = markup Markup.item;
val text_fold = markup Markup.text_fold;
-fun command name = mark_str (Markup.keyword1, name);
-fun keyword name = mark_str (Markup.keyword2, name);
+fun keyword1 name = mark_str (Markup.keyword1, name);
+fun keyword2 name = mark_str (Markup.keyword2, name);
+fun keyword3 name = mark_str (Markup.keyword3, name);
val text = breaks o map str o Symbol.explode_words;
val paragraph = markup Markup.paragraph;
--- a/src/Pure/Isar/bundle.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/Pure/Isar/bundle.ML Wed Feb 26 10:53:19 2014 +0100
@@ -133,7 +133,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.mark_str name ::
+ Pretty.block (Pretty.keyword1 "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/class.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/Pure/Isar/class.ML Wed Feb 26 10:53:19 2014 +0100
@@ -187,7 +187,7 @@
fun prt_entry class =
Pretty.block
- ([Pretty.command "class", Pretty.brk 1,
+ ([Pretty.keyword1 "class", Pretty.brk 1,
Name_Space.pretty ctxt class_space class, Pretty.str ":", Pretty.fbrk,
Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
(case try (Axclass.get_info thy) class of
@@ -530,7 +530,7 @@
Pretty.block (Pretty.breaks
[Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c,
Pretty.str "::", Syntax.pretty_typ lthy ty]);
- in Pretty.command "instantiation" :: map pr_arity tycos @ map pr_param params end;
+ in Pretty.keyword1 "instantiation" :: map pr_arity tycos @ map pr_param params end;
fun conclude lthy =
let
--- a/src/Pure/Isar/element.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/Pure/Isar/element.ML Wed Feb 26 10:53:19 2014 +0100
@@ -113,8 +113,8 @@
fun pretty_items _ _ [] = []
| pretty_items keyword sep (x :: ys) =
- Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] ::
- map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
+ Pretty.block [Pretty.keyword2 keyword, Pretty.brk 1, x] ::
+ map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword2 sep, Pretty.brk 1, y]) ys;
fun pretty_name_atts ctxt (b, atts) sep =
if Attrib.is_empty_binding (b, atts) then []
@@ -129,7 +129,7 @@
let
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
- val prt_terms = separate (Pretty.keyword "and") o map prt_term;
+ val prt_terms = separate (Pretty.keyword2 "and") o map prt_term;
val prt_name_atts = pretty_name_atts ctxt;
fun prt_show (a, ts) =
@@ -138,11 +138,11 @@
fun prt_var (x, SOME T) = Pretty.block
[Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
| prt_var (x, NONE) = Pretty.str (Binding.name_of x);
- val prt_vars = separate (Pretty.keyword "and") o map prt_var;
+ val prt_vars = separate (Pretty.keyword2 "and") o map prt_var;
fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
| prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
- (prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts));
+ (prt_vars xs @ [Pretty.keyword2 "where"] @ prt_terms ts));
in
fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
| Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
@@ -204,9 +204,9 @@
fun thm_name kind th prts =
let val head =
if Thm.has_name_hint th then
- Pretty.block [Pretty.command kind,
+ Pretty.block [Pretty.keyword1 kind,
Pretty.brk 1, Pretty.str (Long_Name.base_name (Thm.get_name_hint th) ^ ":")]
- else Pretty.command kind
+ else Pretty.keyword1 kind
in Pretty.block (Pretty.fbreaks (head :: prts)) end;
fun obtain prop ctxt =
--- a/src/Pure/Isar/locale.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/Pure/Isar/locale.ML Wed Feb 26 10:53:19 2014 +0100
@@ -647,7 +647,7 @@
|> snd |> rev;
in
Pretty.block
- (Pretty.command "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
+ (Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems)
end;
--- a/src/Pure/Isar/named_target.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/Pure/Isar/named_target.ML Wed Feb 26 10:53:19 2014 +0100
@@ -139,7 +139,7 @@
fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
let
val target_name =
- [Pretty.command (if is_class then "class" else "locale"), Pretty.brk 1,
+ [Pretty.keyword1 (if is_class then "class" else "locale"), Pretty.brk 1,
Locale.pretty_name ctxt target];
val fixes =
map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
@@ -156,7 +156,7 @@
else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
in
- Pretty.block [Pretty.command "theory", Pretty.brk 1,
+ Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))] :: body_elems
end;
--- a/src/Pure/Isar/overloading.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/Pure/Isar/overloading.ML Wed Feb 26 10:53:19 2014 +0100
@@ -173,7 +173,7 @@
Pretty.block (Pretty.breaks
[Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c,
Pretty.str "::", Syntax.pretty_typ lthy ty]);
- in Pretty.command "overloading" :: map pr_operation overloading end;
+ in Pretty.keyword1 "overloading" :: map pr_operation overloading end;
fun conclude lthy =
let
--- a/src/Pure/Isar/proof_display.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/Pure/Isar/proof_display.ML Wed Feb 26 10:53:19 2014 +0100
@@ -100,7 +100,7 @@
in
fun pretty_goal_header goal =
- Pretty.block ([Pretty.command "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
+ Pretty.block ([Pretty.keyword1 "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
end;
@@ -113,7 +113,7 @@
fun pretty_goal_facts ctxt s ths =
(Pretty.block o Pretty.fbreaks)
[if s = "" then Pretty.str "this:"
- else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"],
+ else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
Proof_Context.pretty_fact ctxt ("", ths)];
@@ -135,13 +135,13 @@
local
-fun pretty_fact_name (kind, "") = Pretty.command kind
+fun pretty_fact_name (kind, "") = Pretty.keyword1 kind
| pretty_fact_name (kind, name) =
- Pretty.block [Pretty.command kind, Pretty.brk 1,
+ Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
Pretty.str (Long_Name.base_name name), Pretty.str ":"];
fun pretty_facts ctxt =
- flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
+ flat o (separate [Pretty.fbrk, Pretty.keyword2 "and", Pretty.str " "]) o
map (single o Proof_Context.pretty_fact ctxt);
in
@@ -150,7 +150,7 @@
if not do_print orelse kind = "" then ()
else if name = "" then
(Pretty.writeln o Pretty.mark markup)
- (Pretty.block (Pretty.command kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
+ (Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
else
(Pretty.writeln o Pretty.mark markup)
(case facts of
--- a/src/Pure/PIDE/markup.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Feb 26 10:53:19 2014 +0100
@@ -109,6 +109,7 @@
val tokenN: string val token: Properties.T -> T
val keyword1N: string val keyword1: T
val keyword2N: string val keyword2: T
+ val keyword3N: string val keyword3: T
val elapsedN: string
val cpuN: string
val gcN: string
@@ -400,6 +401,7 @@
val (commandN, command) = markup_elem "command";
val (keyword1N, keyword1) = markup_elem "keyword1";
val (keyword2N, keyword2) = markup_elem "keyword2";
+val (keyword3N, keyword3) = markup_elem "keyword3";
val (operatorN, operator) = markup_elem "operator";
val (stringN, string) = markup_elem "string";
val (altstringN, altstring) = markup_elem "altstring";
--- a/src/Pure/Syntax/mixfix.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/Pure/Syntax/mixfix.ML Wed Feb 26 10:53:19 2014 +0100
@@ -50,7 +50,7 @@
local
val quoted = Pretty.quote o Pretty.str;
-val keyword = Pretty.keyword;
+val keyword = Pretty.keyword2;
val parens = Pretty.enclose "(" ")";
val brackets = Pretty.enclose "[" "]";
val int = Pretty.str o string_of_int;
--- a/src/Tools/subtyping.ML Wed Feb 26 10:45:06 2014 +0100
+++ b/src/Tools/subtyping.ML Wed Feb 26 10:53:19 2014 +0100
@@ -1070,7 +1070,7 @@
Pretty.str "<:", Pretty.brk 1,
Syntax.pretty_typ ctxt (Type (b, Us)), Pretty.brk 3,
Pretty.block
- [Pretty.keyword "using", Pretty.brk 1,
+ [Pretty.keyword2 "using", Pretty.brk 1,
Pretty.quote (Syntax.pretty_term ctxt t)]]];
val type_space = Proof_Context.type_space ctxt;