--- a/src/Pure/PIDE/command.ML Mon Dec 07 15:54:07 2020 +0100
+++ b/src/Pure/PIDE/command.ML Mon Dec 07 16:09:06 2020 +0100
@@ -7,7 +7,7 @@
signature COMMAND =
sig
type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option}
- val read_file: Path.T -> Position.T -> Path.T -> Token.file
+ val read_file: Path.T -> Position.T -> bool -> Path.T -> Token.file
val read_thy: Toplevel.state -> theory
val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
blob Exn.result list * int -> Token.T list -> Toplevel.transition
@@ -55,11 +55,11 @@
type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option};
-fun read_file_node file_node master_dir pos src_path =
+fun read_file_node file_node master_dir pos delimited src_path =
let
val _ =
if Context_Position.pide_reports ()
- then Position.report pos Markup.language_path else ();
+ then Position.report pos (Markup.language_path delimited) else ();
val _ =
(case try Url.explode file_node of
NONE => ()
@@ -90,16 +90,19 @@
fun resolve_files master_dir (blobs, blobs_index) toks =
(case Outer_Syntax.parse_spans toks of
- [Command_Span.Span (Command_Span.Command_Span (cmd, _), _)] =>
+ [Command_Span.Span (Command_Span.Command_Span _, _)] =>
(case try (nth toks) blobs_index of
SOME tok =>
let
- val pos = Token.pos_of tok;
+ val source = Token.input_of tok;
+ val pos = Input.pos_of source;
+ val delimited = Input.is_delimited source;
+
fun make_file (Exn.Res {file_node, src_path, content = NONE}) =
Exn.interruptible_capture (fn () =>
- read_file_node file_node master_dir pos src_path) ()
+ read_file_node file_node master_dir pos delimited src_path) ()
| make_file (Exn.Res {file_node, src_path, content = SOME (digest, lines)}) =
- (Position.report pos Markup.language_path;
+ (Position.report pos (Markup.language_path delimited);
Exn.Res (blob_file src_path lines digest file_node))
| make_file (Exn.Exn e) = Exn.Exn e;
val files = map make_file blobs;
--- a/src/Pure/PIDE/markup.ML Mon Dec 07 15:54:07 2020 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Dec 07 16:09:06 2020 +0100
@@ -44,7 +44,7 @@
val language_verbatim: bool -> T
val language_latex: bool -> T
val language_rail: T
- val language_path: T
+ val language_path: bool -> T
val language_mixfix: T
val bindingN: string val binding: T
val entityN: string val entity: string -> string -> T
@@ -344,7 +344,7 @@
val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false};
val language_latex = language' {name = "latex", symbols = false, 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};
+val language_path = language' {name = "path", symbols = false, antiquotes = false};
val language_mixfix =
language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true};
--- a/src/Pure/PIDE/resources.ML Mon Dec 07 15:54:07 2020 +0100
+++ b/src/Pure/PIDE/resources.ML Mon Dec 07 16:09:06 2020 +0100
@@ -44,9 +44,9 @@
val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser
val provide_parse_file: (theory -> Token.file * theory) parser
val loaded_files_current: theory -> bool
- val check_path: Proof.context -> Path.T option -> string * Position.T -> Path.T
- val check_file: Proof.context -> Path.T option -> string * Position.T -> Path.T
- val check_dir: Proof.context -> Path.T option -> string * Position.T -> Path.T
+ val check_path: Proof.context -> Path.T option -> Input.source -> Path.T
+ val check_file: Proof.context -> Path.T option -> Input.source -> Path.T
+ val check_dir: Proof.context -> Path.T option -> Input.source -> Path.T
end;
structure Resources: RESOURCES =
@@ -288,14 +288,16 @@
(* load files *)
fun parse_files make_paths =
- Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
+ Scan.ahead Parse.not_eof -- Parse.path_input >> (fn (tok, source) => fn thy =>
(case Token.get_files tok of
[] =>
let
val master_dir = master_directory thy;
- val pos = Token.pos_of tok;
+ val name = Input.string_of source;
+ val pos = Input.pos_of source;
+ val delimited = Input.is_delimited source;
val src_paths = make_paths (Path.explode name);
- in map (Command.read_file master_dir pos) src_paths end
+ in map (Command.read_file master_dir pos delimited) src_paths end
| files => map Exn.release files));
val parse_file = parse_files single >> (fn f => f #> the_single);
@@ -336,11 +338,15 @@
(* formal check *)
-fun formal_check check_file ctxt opt_dir (name, pos) =
+fun formal_check check_file ctxt opt_dir source =
let
+ val name = Input.string_of source;
+ val pos = Input.pos_of source;
+ val delimited = Input.is_delimited source;
+
+ val _ = Context_Position.report ctxt pos (Markup.language_path delimited);
+
fun err msg = error (msg ^ Position.here pos);
-
- val _ = Context_Position.report ctxt pos Markup.language_path;
val dir =
(case opt_dir of
SOME dir => dir
@@ -348,7 +354,7 @@
val path = dir + Path.explode name handle ERROR msg => err msg;
val _ = Path.expand path handle ERROR msg => err msg;
val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
- val _ = check_file path handle ERROR msg => err msg;
+ val _ : Path.T = check_file path handle ERROR msg => err msg;
in path end;
val check_path = formal_check I;
@@ -360,16 +366,16 @@
local
-fun document_antiq (check: Proof.context -> Path.T option -> string * Position.T -> Path.T) =
- Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
+fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) =
+ Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
let
- val _ = check ctxt NONE (name, pos);
- val latex = Latex.string (Latex.output_ascii_breakable "/" name);
+ val _ = check ctxt NONE source;
+ val latex = Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source));
in Latex.enclose_block "\\isatt{" "}" [latex] end);
fun ML_antiq check =
- Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
- check ctxt (SOME Path.current) (name, pos) |> ML_Syntax.print_path);
+ Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
+ check ctxt (SOME Path.current) source |> ML_Syntax.print_path);
in
--- a/src/Pure/Pure.thy Mon Dec 07 15:54:07 2020 +0100
+++ b/src/Pure/Pure.thy Mon Dec 07 16:09:06 2020 +0100
@@ -135,13 +135,13 @@
(lines, pos0) |-> fold (fn line => fn pos1 =>
let
val pos2 = pos1 |> fold Position.advance (Symbol.explode line);
- val pos = Position.range_position (pos1, pos2);
+ val range = Position.range (pos1, pos2);
val _ =
if line = "" then ()
else if String.isPrefix "#" line then
- Context_Position.report ctxt pos Markup.comment
+ Context_Position.report ctxt (#1 range) Markup.comment
else
- (ignore (Resources.check_dir ctxt (SOME dir) (line, pos))
+ (ignore (Resources.check_dir ctxt (SOME dir) (Input.source true line range))
handle ERROR msg => Output.error_message msg);
in pos2 |> Position.advance "\n" end);
in thy' end)));
@@ -167,9 +167,9 @@
val base_dir =
Scan.optional (\<^keyword>\<open>(\<close> |--
- Parse.!!! (\<^keyword>\<open>in\<close> |-- Parse.position Parse.path --| \<^keyword>\<open>)\<close>)) ("", Position.none);
+ Parse.!!! (\<^keyword>\<open>in\<close> |-- Parse.path_input --| \<^keyword>\<open>)\<close>)) (Input.string "");
- val external_files = Scan.repeat1 (Parse.position Parse.path) -- base_dir;
+ val external_files = Scan.repeat1 Parse.path_input -- base_dir;
val exe = Parse.reserved "exe" >> K true || Parse.reserved "executable" >> K false;
val executable = \<^keyword>\<open>(\<close> |-- Parse.!!! (exe --| \<^keyword>\<open>)\<close>) >> SOME || Scan.succeed NONE;
--- a/src/Pure/Thy/document_antiquotations.ML Mon Dec 07 15:54:07 2020 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Mon Dec 07 16:09:06 2020 +0100
@@ -315,9 +315,15 @@
translate_string (fn c => if c = "%" orelse c = "#" orelse c = "^" then "\\" ^ c else c);
val _ = Theory.setup
- (Thy_Output.antiquotation_raw_embedded \<^binding>\<open>url\<close> (Scan.lift Args.embedded_position)
- (fn ctxt => fn (url, pos) =>
- let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)];
+ (Thy_Output.antiquotation_raw_embedded \<^binding>\<open>url\<close> (Scan.lift Args.embedded_input)
+ (fn ctxt => fn source =>
+ let
+ val url = Input.string_of source;
+ val pos = Input.pos_of source;
+ val delimited = Input.is_delimited source;
+ val _ =
+ Context_Position.reports ctxt
+ [(pos, Markup.language_path delimited), (pos, Markup.url url)];
in Latex.enclose_block "\\url{" "}" [Latex.string (escape_url url)] end));
--- a/src/Pure/Thy/sessions.ML Mon Dec 07 15:54:07 2020 +0100
+++ b/src/Pure/Thy/sessions.ML Mon Dec 07 16:09:06 2020 +0100
@@ -19,44 +19,44 @@
local
-val theory_entry = Parse.theory_name --| Parse.opt_keyword "global";
+val theory_entry = Parse.input Parse.theory_name --| Parse.opt_keyword "global";
val theories =
Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry);
val in_path =
- Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.position Parse.path --| Parse.$$$ ")");
+ Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.path_input --| Parse.$$$ ")");
val document_theories =
- Parse.$$$ "document_theories" |-- Scan.repeat1 (Parse.position Parse.name);
+ Parse.$$$ "document_theories" |-- Scan.repeat1 (Parse.input Parse.theory_name);
val document_files =
Parse.$$$ "document_files" |--
- Parse.!!! (Scan.optional in_path ("document", Position.none)
- -- Scan.repeat1 (Parse.position Parse.path));
+ Parse.!!! (Scan.optional in_path (Input.string "document") -- Scan.repeat1 Parse.path_input);
val prune =
Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.nat --| Parse.$$$ "]")) 0;
val export_files =
Parse.$$$ "export_files" |--
- Parse.!!!
- (Scan.optional in_path ("export", Position.none) -- prune -- Scan.repeat1 Parse.embedded);
+ Parse.!!! (Scan.optional in_path (Input.string "export") -- prune -- Scan.repeat1 Parse.embedded);
+
+fun path_source source path =
+ Input.source (Input.is_delimited source) (Path.implode path) (Input.range_of source);
in
val command_parser =
Parse.session_name --
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] --
- Scan.optional (Parse.$$$ "in" |-- Parse.!!! (Parse.position Parse.path)) (".", Position.none) --
+ Scan.optional (Parse.$$$ "in" |-- Parse.!!! Parse.path_input) (Input.string ".") --
(Parse.$$$ "=" |--
Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
Scan.optional (Parse.$$$ "sessions" |--
Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
- Scan.optional
- (Parse.$$$ "directories" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.path))) [] --
+ Scan.optional (Parse.$$$ "directories" |-- Parse.!!! (Scan.repeat1 Parse.path_input)) [] --
Scan.repeat theories --
Scan.optional document_theories [] --
Scan.repeat document_files --
@@ -84,27 +84,34 @@
ignore (Completion.check_option_value ctxt x y (Options.default ()))
handle ERROR msg => Output.error_message msg);
- fun check_thy (path, pos) =
- ignore (Resources.check_file ctxt (SOME Path.current) (Path.implode path, pos))
+ fun check_thy source =
+ ignore (Resources.check_file ctxt (SOME Path.current) source)
handle ERROR msg => Output.error_message msg;
val _ =
- maps #2 theories |> List.app (fn (s, pos) =>
+ maps #2 theories |> List.app (fn source =>
let
+ val s = Input.string_of source;
+ val pos = Input.pos_of source;
val {node_name, theory_name, ...} =
Resources.import_name session session_dir s
handle ERROR msg => error (msg ^ Position.here pos);
- val theory_path = the_default node_name (Resources.find_theory_file theory_name);
- in check_thy (theory_path, pos) end);
+ val thy_path = the_default node_name (Resources.find_theory_file theory_name);
+ in check_thy (path_source source thy_path) end);
val _ =
directories |> List.app (ignore o Resources.check_dir ctxt (SOME session_dir));
val _ =
- document_theories |> List.app (fn (thy, pos) =>
- (case Resources.find_theory_file thy of
- NONE => Output.error_message ("Unknown theory " ^ quote thy ^ Position.here pos)
- | SOME path => check_thy (path, pos)));
+ document_theories |> List.app (fn source =>
+ let
+ val thy = Input.string_of source;
+ val pos = Input.pos_of source;
+ in
+ (case Resources.find_theory_file thy of
+ NONE => Output.error_message ("Unknown theory " ^ quote thy ^ Position.here pos)
+ | SOME path => check_thy (path_source source path))
+ end);
val _ =
document_files |> List.app (fn (doc_dir, doc_files) =>
--- a/src/Pure/Tools/generated_files.ML Mon Dec 07 15:54:07 2020 +0100
+++ b/src/Pure/Tools/generated_files.ML Mon Dec 07 16:09:06 2020 +0100
@@ -41,7 +41,7 @@
Path.binding -> Input.source -> unit
val compile_generated_files_cmd: Proof.context ->
((string * Position.T) list * (string * Position.T) option) list ->
- ((string * Position.T) list * (string * Position.T)) list ->
+ (Input.source list * Input.source) list ->
((string * Position.T) list * bool option) list ->
string * Position.T -> Input.source -> unit
val execute: Path.T -> Input.source -> string -> string
@@ -319,7 +319,9 @@
(external |> map (fn (raw_files, raw_base_dir) =>
let
val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
- fun check (s, pos) = (Resources.check_file ctxt (SOME base_dir) (s, pos); Path.explode s);
+ fun check source =
+ (Resources.check_file ctxt (SOME base_dir) source;
+ Path.explode (Input.string_of source));
val files = map check raw_files;
in (files, base_dir) end))
((map o apfst o map) Path.explode_binding export)
@@ -380,8 +382,8 @@
fun path_antiquotation binding check =
antiquotation binding
- (Args.context -- Scan.lift (Parse.position Parse.path) >>
- (fn (ctxt, (name, pos)) => (check ctxt (SOME Path.current) (name, pos) |> Path.implode)))
+ (Args.context -- Scan.lift Parse.path_input >>
+ (fn (ctxt, source) => (check ctxt (SOME Path.current) source |> Path.implode)))
(fn {file_type, argument, ...} => #make_string file_type argument);
val _ =
--- a/src/Tools/Code/code_target.ML Mon Dec 07 15:54:07 2020 +0100
+++ b/src/Tools/Code/code_target.ML Mon Dec 07 16:09:06 2020 +0100
@@ -26,7 +26,7 @@
-> (((string * string) * ({physical: bool} * (Path.T * Position.T)) option) * Token.T list) list
-> local_theory -> local_theory
val export_code_cmd: bool -> string list
- -> (((string * string) * ({physical: bool} * (string * Position.T)) option) * Token.T list) list
+ -> (((string * string) * ({physical: bool} * Input.source) option) * Token.T list) list
-> local_theory -> local_theory
val produce_code: Proof.context -> bool -> string list
-> string -> string -> int option -> Token.T list -> (string list * string) list * string option list
@@ -521,23 +521,29 @@
(* code generation *)
-fun prep_destination (location, (s, pos)) =
- if location = {physical = false}
- then (location, Path.explode_pos (s, pos))
- else
- let
- val _ =
- if s = ""
- then error ("Bad bad empty " ^ Markup.markup Markup.keyword2 "file" ^ " argument")
- else ();
- val _ =
- legacy_feature
- (Markup.markup Markup.keyword1 "export_code" ^ " with " ^
- Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos);
- val _ = Position.report pos Markup.language_path;
- val path = #1 (Path.explode_pos (s, pos));
- val _ = Position.report pos (Markup.path (Path.implode_symbolic path));
- in (location, (path, pos)) end;
+fun prep_destination (location, source) =
+ let
+ val s = Input.string_of source
+ val pos = Input.pos_of source
+ val delimited = Input.is_delimited source
+ in
+ if location = {physical = false}
+ then (location, Path.explode_pos (s, pos))
+ else
+ let
+ val _ =
+ if s = ""
+ then error ("Bad bad empty " ^ Markup.markup Markup.keyword2 "file" ^ " argument")
+ else ();
+ val _ =
+ legacy_feature
+ (Markup.markup Markup.keyword1 "export_code" ^ " with " ^
+ Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos);
+ val _ = Position.report pos (Markup.language_path delimited);
+ val path = #1 (Path.explode_pos (s, pos));
+ val _ = Position.report pos (Markup.path (Path.implode_symbolic path));
+ in (location, (path, pos)) end
+ end;
fun export_code all_public cs seris lthy =
let
@@ -715,7 +721,7 @@
-- Scan.optional (\<^keyword>\<open>module_name\<close> |-- Parse.name) ""
-- Scan.option
((\<^keyword>\<open>file_prefix\<close> >> K {physical = false} || \<^keyword>\<open>file\<close> >> K {physical = true})
- -- Parse.!!! (Parse.position Parse.path))
+ -- Parse.!!! Parse.path_input)
-- code_expr_argsP))
>> (fn seri_args => export_code_cmd all_public raw_cs seri_args);