# HG changeset patch # User wenzelm # Date 1607353746 -3600 # Node ID fd8d82c4433b5a202b6d1d7bf7596ce64a032c82 # Parent 6b96464066a031f233ad8e62db1dfb51b89a0a6c more accurate markup (refining 1c59b555ac4a); diff -r 6b96464066a0 -r fd8d82c4433b src/Pure/PIDE/command.ML --- 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; diff -r 6b96464066a0 -r fd8d82c4433b src/Pure/PIDE/markup.ML --- 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}; diff -r 6b96464066a0 -r fd8d82c4433b src/Pure/PIDE/resources.ML --- 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 diff -r 6b96464066a0 -r fd8d82c4433b src/Pure/Pure.thy --- 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>\(\ |-- - Parse.!!! (\<^keyword>\in\ |-- Parse.position Parse.path --| \<^keyword>\)\)) ("", Position.none); + Parse.!!! (\<^keyword>\in\ |-- Parse.path_input --| \<^keyword>\)\)) (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>\(\ |-- Parse.!!! (exe --| \<^keyword>\)\) >> SOME || Scan.succeed NONE; diff -r 6b96464066a0 -r fd8d82c4433b src/Pure/Thy/document_antiquotations.ML --- 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>\url\ (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>\url\ (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)); diff -r 6b96464066a0 -r fd8d82c4433b src/Pure/Thy/sessions.ML --- 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) => diff -r 6b96464066a0 -r fd8d82c4433b src/Pure/Tools/generated_files.ML --- 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 _ = diff -r 6b96464066a0 -r fd8d82c4433b src/Tools/Code/code_target.ML --- 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>\module_name\ |-- Parse.name) "" -- Scan.option ((\<^keyword>\file_prefix\ >> K {physical = false} || \<^keyword>\file\ >> 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);