merged
authorwenzelm
Wed, 26 Jul 2023 13:09:20 +0200
changeset 78466 1a68cd0c57d3
parent 78461 71713dd09c35 (current diff)
parent 78465 4dffc47b7e91 (diff)
child 78467 ab9cc7cda0ec
merged
--- 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;