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