breakable @{file};
authorwenzelm
Sun, 28 Jul 2013 20:50:44 +0200
changeset 52752 587a4610da9e
parent 52751 b65d699f1a7e
child 52753 1165f78c16d8
breakable @{file};
src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sun Jul 28 20:10:59 2013 +0200
+++ b/src/Pure/Thy/thy_load.ML	Sun Jul 28 20:50:44 2013 +0200
@@ -287,7 +287,11 @@
           if File.exists path then ()
           else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
         val _ = Position.report pos (Markup.path name);
-      in Thy_Output.verb_text name end)));
+      in
+        space_explode "/" name
+        |> map Thy_Output.verb_text
+        |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
+      end)));
 
 
 (* global master path *)