some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
authorwenzelm
Mon Mar 10 21:15:29 2014 +0100 (2014-03-10)
changeset 560341c59b555ac4a
parent 56033 513c2b0ea565
child 56035 745f568837f1
some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
src/Pure/PIDE/command.ML
src/Pure/PIDE/markup.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Mon Mar 10 20:27:08 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Mar 10 21:15:29 2014 +0100
     1.3 @@ -91,6 +91,7 @@
     1.4  
     1.5  fun read_file master_dir pos src_path =
     1.6    let
     1.7 +    val _ = Position.report pos Markup.language_path;
     1.8      val full_path = File.check_file (File.full_path master_dir src_path);
     1.9      val _ = Position.report pos (Markup.path (Path.implode full_path));
    1.10      val text = File.read full_path;
    1.11 @@ -117,7 +118,7 @@
    1.12            fun make_file src_path (Exn.Res (_, NONE)) =
    1.13                  Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
    1.14              | make_file src_path (Exn.Res (file, SOME (digest, lines))) =
    1.15 -               (Position.report pos (Markup.path file);
    1.16 +               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file)];
    1.17                  Exn.Res (blob_file src_path lines digest file))
    1.18              | make_file _ (Exn.Exn e) = Exn.Exn e;
    1.19            val src_paths = Keyword.command_files cmd path;
     2.1 --- a/src/Pure/PIDE/markup.ML	Mon Mar 10 20:27:08 2014 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Mon Mar 10 21:15:29 2014 +0100
     2.3 @@ -37,6 +37,7 @@
     2.4    val language_antiquotation: T
     2.5    val language_text: bool -> T
     2.6    val language_rail: T
     2.7 +  val language_path: T
     2.8    val bindingN: string val binding: T
     2.9    val entityN: string val entity: string -> string -> T
    2.10    val get_entity_kind: T -> string option
    2.11 @@ -290,6 +291,7 @@
    2.12    language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
    2.13  val language_text = language' {name = "text", symbols = true, antiquotes = false};
    2.14  val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
    2.15 +val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true};
    2.16  
    2.17  
    2.18  (* formal entities *)
     3.1 --- a/src/Pure/Thy/thy_load.ML	Mon Mar 10 20:27:08 2014 +0100
     3.2 +++ b/src/Pure/Thy/thy_load.ML	Mon Mar 10 21:15:29 2014 +0100
     3.3 @@ -194,6 +194,8 @@
     3.4  
     3.5  fun file_antiq strict ctxt (name, pos) =
     3.6    let
     3.7 +    val _ = Context_Position.report ctxt pos Markup.language_path;
     3.8 +
     3.9      val dir = master_directory (Proof_Context.theory_of ctxt);
    3.10      val path = Path.append dir (Path.explode name)
    3.11        handle ERROR msg => error (msg ^ Position.here pos);
     4.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 10 20:27:08 2014 +0100
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 10 21:15:29 2014 +0100
     4.3 @@ -675,6 +675,7 @@
     4.4  val _ = Theory.setup
     4.5    (antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name))
     4.6      (fn {context = ctxt, ...} => fn (name, pos) =>
     4.7 -      (Context_Position.report ctxt pos (Markup.url name); enclose "\\url{" "}" name)));
     4.8 +      (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
     4.9 +       enclose "\\url{" "}" name)));
    4.10  
    4.11  end;