# HG changeset patch
# User wenzelm
# Date 1394482529 -3600
# Node ID 1c59b555ac4acdc7841facb5e8647bc34b5f3d17
# Parent  513c2b0ea565b49a21deaf4a6bbfde98de389886
some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;

diff -r 513c2b0ea565 -r 1c59b555ac4a src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Mar 10 20:27:08 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Mon Mar 10 21:15:29 2014 +0100
@@ -91,6 +91,7 @@
 
 fun read_file master_dir pos src_path =
   let
+    val _ = Position.report pos Markup.language_path;
     val full_path = File.check_file (File.full_path master_dir src_path);
     val _ = Position.report pos (Markup.path (Path.implode full_path));
     val text = File.read full_path;
@@ -117,7 +118,7 @@
           fun make_file src_path (Exn.Res (_, NONE)) =
                 Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
             | make_file src_path (Exn.Res (file, SOME (digest, lines))) =
-               (Position.report pos (Markup.path file);
+               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file)];
                 Exn.Res (blob_file src_path lines digest file))
             | make_file _ (Exn.Exn e) = Exn.Exn e;
           val src_paths = Keyword.command_files cmd path;
diff -r 513c2b0ea565 -r 1c59b555ac4a src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Mar 10 20:27:08 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Mar 10 21:15:29 2014 +0100
@@ -37,6 +37,7 @@
   val language_antiquotation: T
   val language_text: bool -> T
   val language_rail: T
+  val language_path: T
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
   val get_entity_kind: T -> string option
@@ -290,6 +291,7 @@
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};
 val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
+val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true};
 
 
 (* formal entities *)
diff -r 513c2b0ea565 -r 1c59b555ac4a src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Mon Mar 10 20:27:08 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML	Mon Mar 10 21:15:29 2014 +0100
@@ -194,6 +194,8 @@
 
 fun file_antiq strict ctxt (name, pos) =
   let
+    val _ = Context_Position.report ctxt pos Markup.language_path;
+
     val dir = master_directory (Proof_Context.theory_of ctxt);
     val path = Path.append dir (Path.explode name)
       handle ERROR msg => error (msg ^ Position.here pos);
diff -r 513c2b0ea565 -r 1c59b555ac4a src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Mar 10 20:27:08 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Mar 10 21:15:29 2014 +0100
@@ -675,6 +675,7 @@
 val _ = Theory.setup
   (antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name))
     (fn {context = ctxt, ...} => fn (name, pos) =>
-      (Context_Position.report ctxt pos (Markup.url name); enclose "\\url{" "}" name)));
+      (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
+       enclose "\\url{" "}" name)));
 
 end;