some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
--- 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;
--- 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 *)
--- 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);
--- 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;