# HG changeset patch # User wenzelm # Date 1690369760 -7200 # Node ID 1a68cd0c57d331ee32bc7dc1278fd9f459882e83 # Parent 71713dd09c35d3055c30e71e524922d78fbf84b6# Parent 4dffc47b7e914a7038c5826156e6b6d13c08ee52 merged diff -r 71713dd09c35 -r 1a68cd0c57d3 src/HOL/Library/conditional_parametricity.ML --- a/src/HOL/Library/conditional_parametricity.ML Wed Jul 26 12:04:25 2023 +0200 +++ b/src/HOL/Library/conditional_parametricity.ML Wed Jul 26 13:09:20 2023 +0200 @@ -502,7 +502,7 @@ val thm = prove_goal settings lthy (SOME eq) goal; val (res, lthy') = Local_Theory.note (b, [thm]) lthy; val _ = if #suppress_print_theorem settings then () else - Proof_Display.print_results true (Position.thread_data ()) lthy' (("theorem",""), [res]); + Proof_Display.print_theorem (Position.thread_data ()) lthy' res; in (the_single (snd res), lthy') end; diff -r 71713dd09c35 -r 1a68cd0c57d3 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Wed Jul 26 12:04:25 2023 +0200 +++ b/src/Pure/Isar/proof_display.ML Wed Jul 26 13:09:20 2023 +0200 @@ -26,6 +26,7 @@ val show_results: bool Config.T val print_results: bool -> Position.T -> Proof.context -> ((string * string) * (string * thm list) list) -> unit + val print_theorem: Position.T -> Proof.context -> string * thm list -> unit val print_consts: bool -> Position.T -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit val markup_extern_label: Position.T -> (Markup.T * xstring) option @@ -362,6 +363,9 @@ | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk, Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])); +fun print_theorem pos ctxt fact = + print_results true pos ctxt ((Thm.theoremK, ""), [fact]); + end; diff -r 71713dd09c35 -r 1a68cd0c57d3 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Wed Jul 26 12:04:25 2023 +0200 +++ b/src/Pure/PIDE/markup.ML Wed Jul 26 13:09:20 2023 +0200 @@ -11,8 +11,10 @@ val is_empty: T -> bool val properties: Properties.T -> T -> T val nameN: string val name: string -> T -> T + val name_proper: string -> Properties.T val xnameN: string val xname: string -> T -> T - val kindN: string + val kindN: string val kind: string -> T -> T + val kind_proper: string -> Properties.T val serialN: string val serial_properties: int -> Properties.T val instanceN: string @@ -312,11 +314,14 @@ val nameN = "name"; fun name a = properties [(nameN, a)]; +val name_proper = Properties.make_string nameN; val xnameN = "xname"; fun xname a = properties [(xnameN, a)]; val kindN = "kind"; +fun kind a = properties [(kindN, a)]; +val kind_proper = Properties.make_string kindN; val serialN = "serial"; fun serial_properties i = [(serialN, Value.print_int i)]; @@ -385,9 +390,7 @@ val (bindingN, binding) = markup_elem "binding"; val entityN = "entity"; -fun entity kind name = - (entityN, - (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)])); +fun entity kind name = (entityN, name_proper name @ kind_proper kind); val defN = "def"; val refN = "ref"; @@ -434,7 +437,7 @@ (* expression *) val expressionN = "expression"; -fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]); +fun expression kind = (expressionN, kind_proper kind); (* citation *) @@ -597,9 +600,7 @@ val (latex_bodyN, latex_body) = markup_string "latex_body" kindN; val (latex_citeN, _) = markup_elem "latex_cite"; fun latex_cite {kind, citations} = - (latex_citeN, - (if kind = "" then [] else [(kindN, kind)]) @ - (if citations = "" then [] else [("citations", citations)])); + (latex_citeN, kind_proper kind @ Properties.make_string "citations" citations); val (latex_index_itemN, latex_index_item) = markup_elem "latex_index_item"; val (latex_index_entryN, latex_index_entry) = markup_string "latex_index_entry" kindN; val (latex_delimN, latex_delim) = markup_string "latex_delim" nameN; @@ -632,9 +633,7 @@ val (command_keywordN, command_keyword) = markup_elem "command_keyword"; val command_spanN = "command_span"; -fun command_span {name, kind} : T = - (command_spanN, - (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)])); +fun command_span {name, kind} : T = (command_spanN, name_proper name @ kind_proper kind); val commandN = "command"; val command_properties = properties [(kindN, commandN)]; val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)]; diff -r 71713dd09c35 -r 1a68cd0c57d3 src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML Wed Jul 26 12:04:25 2023 +0200 +++ b/src/Pure/Thy/bibtex.ML Wed Jul 26 13:09:20 2023 +0200 @@ -49,7 +49,7 @@ fun decode yxml = let val props = XML.Decode.properties (YXML.parse_body yxml); - val name = the_default "" (Properties.get props Markup.nameN); + val name = Properties.get_string props Markup.nameN; val pos = Position.of_properties props; in (name, pos) end; in diff -r 71713dd09c35 -r 1a68cd0c57d3 src/Pure/context.ML --- a/src/Pure/context.ML Wed Jul 26 12:04:25 2023 +0200 +++ b/src/Pure/context.ML Wed Jul 26 13:09:20 2023 +0200 @@ -204,8 +204,12 @@ local +val m = Integer.pow 18 2; + fun cons_tokens var token = - Synchronized.change var (fn (n, tokens) => (n + 1, Weak.weak (SOME token) :: tokens)); + Synchronized.change var (fn (n, tokens) => + let val tokens' = if n mod m = 0 then filter Unsynchronized.weak_active tokens else tokens + in (n + 1, Weak.weak (SOME token) :: tokens') end); fun finish_tokens var = Synchronized.change_result var (fn (n, tokens) => diff -r 71713dd09c35 -r 1a68cd0c57d3 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Wed Jul 26 12:04:25 2023 +0200 +++ b/src/Pure/more_thm.ML Wed Jul 26 13:09:20 2023 +0200 @@ -615,7 +615,7 @@ val theoremK = "theorem"; -fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); +fun legacy_get_kind thm = Properties.get_string (Thm.get_tags thm) Markup.kindN; fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;