1.1 --- a/src/Doc/antiquote_setup.ML Thu Mar 13 10:34:48 2014 +0100
1.2 +++ b/src/Doc/antiquote_setup.ML Thu Mar 13 11:34:05 2014 +0100
1.3 @@ -166,12 +166,12 @@
1.4 | parse_named _ _ = [];
1.5
1.6 val jedit_actions =
1.7 - (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/actions.xml")) of
1.8 + (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
1.9 XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
1.10 | _ => []);
1.11
1.12 val jedit_dockables =
1.13 - (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/dockables.xml")) of
1.14 + (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
1.15 XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
1.16 | _ => []);
1.17