--- a/src/Pure/Tools/jedit.ML Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Pure/Tools/jedit.ML Thu Aug 11 18:26:44 2016 +0200
@@ -24,13 +24,13 @@
val isabelle_jedit_actions =
Lazy.lazy (fn () =>
- (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
+ (case XML.parse (File.read @{file "~~/src/Tools/jEdit/src/actions.xml"}) of
XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
| _ => []));
val isabelle_jedit_dockables =
Lazy.lazy (fn () =>
- (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
+ (case XML.parse (File.read @{file "~~/src/Tools/jEdit/src/dockables.xml"}) of
XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
| _ => []));