src/Pure/PIDE/resources.ML
changeset 58716 23a380cc45f4
parent 57918 f5d73caba4e5
child 58741 6e7b009e6d94
     1.1 --- a/src/Pure/PIDE/resources.ML	Mon Oct 20 14:11:14 2014 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Mon Oct 20 16:52:36 2014 +0200
     1.3 @@ -222,8 +222,9 @@
     1.4      val _ = check_path strict ctxt dir (name, pos);
     1.5    in
     1.6      space_explode "/" name
     1.7 -    |> map Thy_Output.verb_text
     1.8 -    |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
     1.9 +    |> map Latex.output_ascii
    1.10 +    |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
    1.11 +    |> Thy_Output.enclose_isabelle_tt ctxt
    1.12    end;
    1.13  
    1.14  in