# HG changeset patch # User wenzelm # Date 1553975687 -3600 # Node ID c8e08d8ffb93373bcf24718f03416d8296724457 # Parent 7a9c559bc518639b20eae94b4a5af409f4601798 clarified signature: more explicit type Path.binding; tuned; diff -r 7a9c559bc518 -r c8e08d8ffb93 etc/symbols --- a/etc/symbols Sat Mar 30 12:07:31 2019 +0100 +++ b/etc/symbols Sat Mar 30 20:54:47 2019 +0100 @@ -408,6 +408,7 @@ \<^named_theorems> argument: cartouche \<^nonterminal> argument: cartouche \<^path> argument: cartouche +\<^path_binding> argument: cartouche \<^plugin> argument: cartouche \<^print> \<^prop> argument: cartouche diff -r 7a9c559bc518 -r c8e08d8ffb93 lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Sat Mar 30 12:07:31 2019 +0100 +++ b/lib/texinputs/isabellesym.sty Sat Mar 30 20:54:47 2019 +0100 @@ -394,6 +394,7 @@ \newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}} \newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}} \newcommand{\isactrlpath}{\isakeywordcontrol{path}} +\newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}} \newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}} \newcommand{\isactrlprint}{\isakeywordcontrol{print}} \newcommand{\isactrlprop}{\isakeywordcontrol{prop}} diff -r 7a9c559bc518 -r c8e08d8ffb93 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Sat Mar 30 12:07:31 2019 +0100 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sat Mar 30 20:54:47 2019 +0100 @@ -973,7 +973,7 @@ \because their proofs contain oracles:" proved')); val prv_path = Path.ext "prv" path; val _ = - Export.export thy prv_path + Export.export thy (Path.binding (prv_path, Position.none)) [implode (map (fn (s, _) => snd (strip_number s) ^ " -- proved by " ^ Distribution.version ^ "\n") proved'')]; in {pfuns = pfuns, type_map = type_map, env = NONE} end)) diff -r 7a9c559bc518 -r c8e08d8ffb93 src/Pure/General/path.ML --- a/src/Pure/General/path.ML Sat Mar 30 12:07:31 2019 +0100 +++ b/src/Pure/General/path.ML Sat Mar 30 20:54:47 2019 +0100 @@ -19,12 +19,12 @@ val has_parent: T -> bool val is_absolute: T -> bool val is_basic: T -> bool - val all_basic: T -> bool val starts_basic: T -> bool val append: T -> T -> T val appends: T list -> T val implode: T -> string val explode: string -> T + val explode_pos: string * Position.T -> T * Position.T val decode: T XML.Decode.T val split: string -> T list val pretty: T -> Pretty.T @@ -38,6 +38,14 @@ val file_name: T -> string val smart_implode: T -> string val position: T -> Position.T + eqtype binding + val binding: T * Position.T -> binding + val binding0: T -> binding + val binding_map: (T -> T) -> binding -> binding + val dest_binding: binding -> T * Position.T + val implode_binding: binding -> string + val explode_binding: string * Position.T -> binding + val explode_binding0: string -> binding end; structure Path: PATH = @@ -169,6 +177,9 @@ in Path (norm (rev elems @ roots)) end; +fun explode_pos (s, pos) = + (explode_path s handle ERROR msg => error (msg ^ Position.here pos), pos); + fun split str = space_explode ":" str |> map_filter (fn s => if s = "" then NONE else SOME (explode_path s)); @@ -243,6 +254,26 @@ val position = Position.file o smart_implode; + +(* binding: strictly monotonic path with position *) + +datatype binding = Binding of T * Position.T; + +fun binding (path, pos) = + if not (is_current path) andalso all_basic path then Binding (path, pos) + else error ("Bad path binding: " ^ print path ^ Position.here pos); + +fun binding0 path = binding (path, Position.none); +fun binding_map f (Binding (path, pos)) = binding (f path, pos); + +fun dest_binding (Binding args) = args; + +val implode_binding = dest_binding #> #1 #> implode_path; + +val explode_binding = binding o explode_pos; +fun explode_binding0 s = explode_binding (s, Position.none); + + (*final declarations of this structure!*) val implode = implode_path; val explode = explode_path; diff -r 7a9c559bc518 -r c8e08d8ffb93 src/Pure/ML/ml_syntax.ML --- a/src/Pure/ML/ml_syntax.ML Sat Mar 30 12:07:31 2019 +0100 +++ b/src/Pure/ML/ml_syntax.ML Sat Mar 30 20:54:47 2019 +0100 @@ -23,6 +23,7 @@ val print_properties: Properties.T -> string val print_position: Position.T -> string val print_range: Position.range -> string + val print_path_binding: Path.binding -> string val make_binding: string * Position.T -> string val print_indexname: indexname -> string val print_class: class -> string @@ -98,6 +99,9 @@ fun print_range range = "Position.range_of_properties " ^ print_properties (Position.properties_of_range range); +fun print_path_binding binding = + "Path.binding " ^ print_pair print_path print_position (Path.dest_binding binding); + fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos); diff -r 7a9c559bc518 -r c8e08d8ffb93 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Sat Mar 30 12:07:31 2019 +0100 +++ b/src/Pure/PIDE/resources.ML Sat Mar 30 20:54:47 2019 +0100 @@ -290,6 +290,9 @@ ML_Antiquotation.value_embedded \<^binding>\path\ (ML_antiq check_path) #> ML_Antiquotation.value_embedded \<^binding>\file\ (ML_antiq check_file) #> ML_Antiquotation.value_embedded \<^binding>\dir\ (ML_antiq check_dir) #> + ML_Antiquotation.value_embedded \<^binding>\path_binding\ + (Scan.lift (Parse.position Parse.path) >> + (ML_Syntax.print_path_binding o Path.explode_binding)) #> ML_Antiquotation.value \<^binding>\master_dir\ (Args.theory >> (ML_Syntax.print_path o master_directory))); diff -r 7a9c559bc518 -r c8e08d8ffb93 src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Sat Mar 30 12:07:31 2019 +0100 +++ b/src/Pure/Thy/export.ML Sat Mar 30 20:54:47 2019 +0100 @@ -6,13 +6,12 @@ signature EXPORT = sig - val check_name: Path.T -> string - type params = {theory: theory, path: Path.T, executable: bool, compress: bool} + type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool} val export_params: params -> string list -> unit - val export: theory -> Path.T -> string list -> unit - val export_executable: theory -> Path.T -> string list -> unit - val export_file: theory -> Path.T -> Path.T -> unit - val export_executable_file: theory -> Path.T -> Path.T -> unit + val export: theory -> Path.binding -> string list -> unit + val export_executable: theory -> Path.binding -> string list -> unit + val export_file: theory -> Path.binding -> Path.T -> unit + val export_executable_file: theory -> Path.binding -> Path.T -> unit val markup: theory -> Path.T -> Markup.T val message: theory -> Path.T -> string end; @@ -22,33 +21,25 @@ (* export *) -fun check_name path = - let - val name = Path.implode path; - val _ = - if not (Path.is_current path) andalso Path.all_basic path then () - else error ("Bad export name: " ^ quote name); - in name end; +type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool}; -type params = {theory: theory, path: Path.T, executable: bool, compress: bool}; - -fun export_params ({theory, path, executable, compress}: params) blob = +fun export_params ({theory, binding, executable, compress}: params) blob = (Output.try_protocol_message o Markup.export) {id = Position.get_id (Position.thread_data ()), serial = serial (), theory_name = Context.theory_long_name theory, - name = check_name path, + name = Path.implode_binding binding, executable = executable, compress = compress} blob; -fun export thy path blob = - export_params {theory = thy, path = path, executable = false, compress = true} blob; +fun export thy binding blob = + export_params {theory = thy, binding = binding, executable = false, compress = true} blob; -fun export_executable thy path blob = - export_params {theory = thy, path = path, executable = true, compress = true} blob; +fun export_executable thy binding blob = + export_params {theory = thy, binding = binding, executable = true, compress = true} blob; -fun export_file thy path file = export thy path [File.read file]; -fun export_executable_file thy path file = export_executable thy path [File.read file]; +fun export_file thy binding file = export thy binding [File.read file]; +fun export_executable_file thy binding file = export_executable thy binding [File.read file]; (* information message *) diff -r 7a9c559bc518 -r c8e08d8ffb93 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sat Mar 30 12:07:31 2019 +0100 +++ b/src/Pure/Thy/export_theory.ML Sat Mar 30 20:54:47 2019 +0100 @@ -172,7 +172,7 @@ if Options.bool (#options context) "export_theory" then f context thy else ())); fun export_body thy name body = - Export.export thy (Path.make ["theory", name]) + Export.export thy (Path.binding0 (Path.make ["theory", name])) (Buffer.chunks (YXML.buffer_body body Buffer.empty)); diff -r 7a9c559bc518 -r c8e08d8ffb93 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sat Mar 30 12:07:31 2019 +0100 +++ b/src/Pure/Thy/thy_info.ML Sat Mar 30 20:54:47 2019 +0100 @@ -66,7 +66,7 @@ val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; val _ = if Options.bool options "export_document" - then Export.export thy (Path.explode "document.tex") output else (); + then Export.export thy (Path.explode_binding0 "document.tex") output else (); val _ = if #enabled option then Present.theory_output thy output else (); in () end end)); diff -r 7a9c559bc518 -r c8e08d8ffb93 src/Pure/Tools/generated_files.ML --- a/src/Pure/Tools/generated_files.ML Sat Mar 30 12:07:31 2019 +0100 +++ b/src/Pure/Tools/generated_files.ML Sat Mar 30 20:54:47 2019 +0100 @@ -6,7 +6,7 @@ signature GENERATED_FILES = sig - val add_files: (Path.T * Position.T) * string -> theory -> theory + val add_files: Path.binding * string -> theory -> theory val get_files: theory -> {path: Path.T, pos: Position.T, content: string} list val write_files: theory -> Path.T -> (Path.T * Position.T) list val export_files: theory -> theory list -> (Path.T * Position.T) list @@ -53,18 +53,12 @@ (* files *) -fun add_files ((path0, pos), content) = - let - val path = Path.expand path0; - fun err msg ps = error (msg ^ ": " ^ Path.print path ^ Position.here_list ps); - val _ = - if Path.is_absolute path then err "Illegal absolute path" [pos] - else if Path.has_parent path then err "Illegal parent path" [pos] - else (); - in +fun add_files (binding, content) = + let val (path, pos) = Path.dest_binding binding in (Data.map o @{apply 3(1)}) (fn files => (case AList.lookup (op =) files path of - SOME (pos', _) => err "Duplicate generated file" [pos, pos'] + SOME (pos', _) => + error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos']) | NONE => (path, (pos, content)) :: files)) end; @@ -83,7 +77,7 @@ fun export_files thy other_thys = other_thys |> maps (fn other_thy => get_files other_thy |> map (fn {path, pos, content} => - (Export.export thy path [content]; (path, pos)))); + (Export.export thy (Path.binding (path, pos)) [content]; (path, pos)))); fun the_file_content thy path = (case find_first (fn file => #path file = path) (get_files thy) of @@ -175,13 +169,14 @@ val thy = Proof_Context.theory_of lthy; val path = Path.explode file; + val binding = Path.binding (path, pos); val file_type = the_file_type thy (#2 (Path.split_ext path)) handle ERROR msg => error (msg ^ Position.here pos); val header = #make_comment file_type " generated by Isabelle "; val content = header ^ "\n" ^ read_source lthy file_type source; - in lthy |> (Local_Theory.background_theory o add_files) ((path, pos), content) end; + in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end; diff -r 7a9c559bc518 -r c8e08d8ffb93 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Sat Mar 30 12:07:31 2019 +0100 +++ b/src/Tools/Code/code_target.ML Sat Mar 30 20:54:47 2019 +0100 @@ -11,8 +11,9 @@ datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list; - val export_code_for: ({physical: bool} * Path.T) option -> string -> string -> int option -> Token.T list - -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory + val export_code_for: ({physical: bool} * (Path.T * Position.T)) option -> string -> string + -> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list + -> local_theory -> local_theory val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list val present_code_for: Proof.context -> string -> string -> int option -> Token.T list @@ -21,7 +22,7 @@ -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory val export_code: bool -> string list - -> (((string * string) * ({physical: bool} * Path.T) option) * Token.T list) list + -> (((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 @@ -273,13 +274,14 @@ local -fun export_logical file_prefix format pretty_modules = +fun export_logical (file_prefix, file_pos) format pretty_modules = let val prefix = Path.append (Path.basic codeN) file_prefix; fun export path content thy = let - val thy' = thy |> Generated_Files.add_files ((path, Position.none), content); - val _ = Export.export thy' path [content]; + val binding = Path.binding (path, file_pos); + val thy' = thy |> Generated_Files.add_files (binding, content); + val _ = Export.export thy' binding [content]; in thy' end; in (case pretty_modules of @@ -303,10 +305,10 @@ (case some_file of NONE => let val (file_prefix, thy') = next_export thy; - in export_logical (Path.basic file_prefix) format pretty_code thy' end + in export_logical (Path.basic file_prefix, Position.none) format pretty_code thy' end | SOME ({physical = false}, file_prefix) => export_logical file_prefix format pretty_code thy - | SOME ({physical = true}, file) => + | SOME ({physical = true}, (file, _)) => let val root = File.full_path (Resources.master_directory thy) file; val _ = File.check_dir (Path.dir root); @@ -448,7 +450,7 @@ val destination = make_destination p; val lthy' = lthy |> Local_Theory.background_theory - (export_result (SOME ({physical = true}, destination)) format + (export_result (SOME ({physical = true}, (destination, Position.none))) format (invoke_serializer lthy target_name generatedN args program all_public syms)); val cmd = make_command generatedN; val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1"; @@ -503,11 +505,8 @@ (* code generation *) fun prep_destination (location, (s, pos)) = - if location = {physical = false} then - let - val path = (Path.explode s |> tap Export.check_name) - handle ERROR msg => error (msg ^ Position.here pos) - in (location, path) end + if location = {physical = false} + then (location, Path.explode_pos (s, pos)) else let val _ = @@ -519,9 +518,9 @@ (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 = Path.explode s; + val path = #1 (Path.explode_pos (s, pos)); val _ = Position.report pos (Markup.path (Path.smart_implode path)); - in (location, path) end; + in (location, (path, pos)) end; fun export_code all_public cs seris lthy = let