# HG changeset patch
# User wenzelm
# Date 1428398754 -7200
# Node ID 83071f4c8ae6dc197b61a43adf50551ae00e485d
# Parent  e83ecf0a0ee19bdb63da91aea90659dbc185657f
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;

diff -r e83ecf0a0ee1 -r 83071f4c8ae6 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 => ()