tuned output of plain name;
authorwenzelm
Fri, 19 Jan 2018 11:34:41 +0100
changeset 67468 aa8c25c528c0
parent 67467 482b62d694ca
child 67469 008725a1ed52
tuned output of plain name;
src/Doc/antiquote_setup.ML
src/Pure/Thy/document_antiquotations.ML
--- a/src/Doc/antiquote_setup.ML	Fri Jan 19 11:26:31 2018 +0100
+++ b/src/Doc/antiquote_setup.ML	Fri Jan 19 11:34:41 2018 +0100
@@ -127,8 +127,7 @@
         Output.output
           (Document_Antiquotation.format ctxt
             (Document_Antiquotation.quote ctxt (Thy_Output.pretty_thm ctxt thm))) ^
-        enclose "\\rulename{" "}"
-          (Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name))))
+        enclose "\\rulename{" "}" (Output.output name))
       #> space_implode "\\par\\smallskip%\n"
       #> Latex.string #> single
       #> Thy_Output.isabelle ctxt));
--- a/src/Pure/Thy/document_antiquotations.ML	Fri Jan 19 11:26:31 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Fri Jan 19 11:34:41 2018 +0100
@@ -296,7 +296,7 @@
   (Thy_Output.antiquotation_pretty \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
     (fn ctxt => fn (name, pos) =>
       let val _ = Context_Position.report ctxt pos (Markup.doc name)
-      in [Thy_Output.pretty_text ctxt name] end));
+      in [Pretty.str name] end));
 
 
 (* formal entities *)