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.
clarified unbreakable latex output: Pretty.unformatted and (Pretty.string_of o Pretty.unbreakable) should coincide, but are produced by quite different means;
authorwenzelm
Tue, 10 Sep 2024 14:53:04 +0200
changeset 80842 4d39ba5f82d6
parent 80841 1beb2dc3bf14
child 80843 67f5861415a5
clarified unbreakable latex output: Pretty.unformatted and (Pretty.string_of o Pretty.unbreakable) should coincide, but are produced by quite different means;
src/Pure/Thy/document_antiquotation.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Thy/document_antiquotation.ML	Tue Sep 10 12:34:32 2024 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Tue Sep 10 14:53:04 2024 +0200
@@ -83,9 +83,10 @@
   Config.get ctxt thy_output_display ? Pretty.indent (Config.get ctxt thy_output_indent);
 
 fun format ctxt =
-  if Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break
-  then Pretty.string_of_ops (Pretty.output_ops (SOME (Config.get ctxt thy_output_margin)))
-  else Pretty.unformatted_string_of;
+  let
+    val breakable = Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break;
+    val ops = Pretty.output_ops (SOME (Config.get ctxt thy_output_margin));
+  in not breakable ? Pretty.unbreakable #> Pretty.string_of_ops ops end;
 
 fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Output.output;
isabelle