--- 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;
--- 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;
--- 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)];
--- 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
--- 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) =>
--- 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;