Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 24 Sep 2024 17:41:05 +0200
changeset 80939 3eca969b3c43
parent 80938 a119154a5f27
child 80940 334625aec7a4
tuned;
src/Pure/General/binding.ML file | annotate | diff | comparison | revisions
src/Pure/Tools/find_consts.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/General/binding.ML	Tue Sep 24 17:35:24 2024 +0200
+++ b/src/Pure/General/binding.ML	Tue Sep 24 17:41:05 2024 +0200
@@ -177,7 +177,7 @@
 fun pretty b =
   if is_empty b then Pretty.str "\"\""
   else
-    Pretty.mark (Position.markup_properties (pos_of b) Markup.binding) (Pretty.str (long_name_of b))
+    Pretty.mark_str (Position.markup_properties (pos_of b) Markup.binding, long_name_of b)
     |> Pretty.quote;
 
 val print = Pretty.unformatted_string_of o pretty;
--- a/src/Pure/Tools/find_consts.ML	Tue Sep 24 17:35:24 2024 +0200
+++ b/src/Pure/Tools/find_consts.ML	Tue Sep 24 17:41:05 2024 +0200
@@ -65,7 +65,7 @@
     val markup = Name_Space.markup (Proof_Context.const_space ctxt) c;
   in
     Pretty.block
-     [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
+     [Pretty.mark_str (markup, c), Pretty.str " ::", Pretty.brk 1,
       Pretty.quote (Syntax.pretty_typ ctxt ty')]
   end;
isabelle