# HG changeset patch
# User wenzelm
# Date 1375037444 -7200
# Node ID 587a4610da9ef693daf5db3dc4c8c5a38ca86316
# Parent  b65d699f1a7e83ef1cc4a2569cb69bc2eb4d7f49
breakable @{file};

diff -r b65d699f1a7e -r 587a4610da9e 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 *)