diff -r 4a7a07c01857 -r efa24d31e595 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Thu Mar 13 10:34:48 2014 +0100 +++ b/src/Doc/antiquote_setup.ML Thu Mar 13 11:34:05 2014 +0100 @@ -166,12 +166,12 @@ | parse_named _ _ = []; val jedit_actions = - (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/actions.xml")) of + (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body | _ => []); val jedit_dockables = - (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/dockables.xml")) of + (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body | _ => []);