--- a/src/Pure/Tools/jedit.ML Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Pure/Tools/jedit.ML Fri Aug 12 17:53:55 2016 +0200
@@ -24,13 +24,13 @@
val isabelle_jedit_actions =
Lazy.lazy (fn () =>
- (case XML.parse (File.read @{file "~~/src/Tools/jEdit/src/actions.xml"}) of
+ (case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/actions.xml\<close>) of
XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
| _ => []));
val isabelle_jedit_dockables =
Lazy.lazy (fn () =>
- (case XML.parse (File.read @{file "~~/src/Tools/jEdit/src/dockables.xml"}) of
+ (case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/dockables.xml\<close>) of
XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
| _ => []));