recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;
authorwenzelm
Tue, 07 Apr 2015 11:25:54 +0200
changeset 59944 83071f4c8ae6
parent 59943 e83ecf0a0ee1
child 59945 cfbaee8cdf1d
recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;
src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Tue Apr 07 10:13:33 2015 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Apr 07 11:25:54 2015 +0200
@@ -51,6 +51,7 @@
 
 fun read_file_node file_node master_dir pos src_path =
   let
+    val _ = Position.report pos Markup.language_path;
     val _ =
       (case try Url.explode file_node of
         NONE => ()