--- 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 *)