# HG changeset patch
# User wenzelm
# Date 1590525905 -7200
# Node ID 9a12eb655f67debbde6c097e8ff69ae86e56ff1f
# Parent  4df3412493480c3b51a7cc098092838e13e0faa1
tuned signature;

diff -r 4df341249348 -r 9a12eb655f67 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Tue May 26 19:59:13 2020 +0200
+++ b/src/Pure/PIDE/resources.ML	Tue May 26 22:45:05 2020 +0200
@@ -293,11 +293,8 @@
   Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
     let
       val _ = check ctxt NONE (name, pos);
-      val latex =
-        space_explode "/" name
-        |> map Latex.output_ascii
-        |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}");
-    in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end);
+      val latex = Latex.string (Latex.output_ascii_breakable "/" name);
+    in Latex.enclose_block "\\isatt{" "}" [latex] end);
 
 fun ML_antiq check =
   Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
diff -r 4df341249348 -r 9a12eb655f67 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue May 26 19:59:13 2020 +0200
+++ b/src/Pure/Thy/latex.ML	Tue May 26 22:45:05 2020 +0200
@@ -16,6 +16,7 @@
   val output_positions: Position.T -> text list -> string
   val output_name: string -> string
   val output_ascii: string -> string
+  val output_ascii_breakable: string -> string -> string
   val output_symbols: Symbol.symbol list -> string
   val output_syms: string -> string
   val symbols: Symbol_Pos.T list -> text
@@ -117,6 +118,11 @@
           if exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~"
           then enclose "{\\char`\\" "}" s else s);
 
+fun output_ascii_breakable sep =
+  space_explode sep
+  #> map output_ascii
+  #> space_implode (output_ascii sep ^ "\\discretionary{}{}{}");
+
 
 (* output symbols *)