# HG changeset patch # User wenzelm # Date 1393408399 -3600 # Node ID 4b3907cb565405207b7248fc7b4acc0139b403dd # Parent 27a45aec67a0d67fee54e58e52ab7df3404e5072 tuned signature; diff -r 27a45aec67a0 -r 4b3907cb5654 src/HOL/Tools/Datatype/datatype_data.ML --- 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))); diff -r 27a45aec67a0 -r 4b3907cb5654 src/Pure/General/pretty.ML --- 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; diff -r 27a45aec67a0 -r 4b3907cb5654 src/Pure/Isar/bundle.ML --- 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)) diff -r 27a45aec67a0 -r 4b3907cb5654 src/Pure/Isar/class.ML --- 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 diff -r 27a45aec67a0 -r 4b3907cb5654 src/Pure/Isar/element.ML --- 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 = diff -r 27a45aec67a0 -r 4b3907cb5654 src/Pure/Isar/locale.ML --- 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; diff -r 27a45aec67a0 -r 4b3907cb5654 src/Pure/Isar/named_target.ML --- 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; diff -r 27a45aec67a0 -r 4b3907cb5654 src/Pure/Isar/overloading.ML --- 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 diff -r 27a45aec67a0 -r 4b3907cb5654 src/Pure/Isar/proof_display.ML --- 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 diff -r 27a45aec67a0 -r 4b3907cb5654 src/Pure/PIDE/markup.ML --- 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"; diff -r 27a45aec67a0 -r 4b3907cb5654 src/Pure/Syntax/mixfix.ML --- 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; diff -r 27a45aec67a0 -r 4b3907cb5654 src/Tools/subtyping.ML --- 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;