--- 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
--- 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}}
--- 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))
--- 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;
--- 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);
--- 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>\<open>path\<close> (ML_antiq check_path) #>
ML_Antiquotation.value_embedded \<^binding>\<open>file\<close> (ML_antiq check_file) #>
ML_Antiquotation.value_embedded \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
+ ML_Antiquotation.value_embedded \<^binding>\<open>path_binding\<close>
+ (Scan.lift (Parse.position Parse.path) >>
+ (ML_Syntax.print_path_binding o Path.explode_binding)) #>
ML_Antiquotation.value \<^binding>\<open>master_dir\<close>
(Args.theory >> (ML_Syntax.print_path o master_directory)));
--- 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 *)
--- 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));
--- 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));
--- 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;
--- 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