clarified signature: Path.T as in Generated_Files;
authorwenzelm
Sat Feb 02 15:52:14 2019 +0100 (3 months ago)
changeset 6978424bbc4e30e5b
parent 69783 dde776d1defa
child 69785 9e326f6f8a24
clarified signature: Path.T as in Generated_Files;
src/HOL/SPARK/Tools/spark_vcs.ML
src/Pure/General/path.ML
src/Pure/Thy/export.ML
src/Pure/Thy/export_theory.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/generated_files.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Feb 02 14:51:11 2019 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Feb 02 15:52:14 2019 +0100
     1.3 @@ -973,7 +973,7 @@
     1.4               \because their proofs contain oracles:" proved'));
     1.5            val prv_path = Path.ext "prv" path;
     1.6            val _ =
     1.7 -            Export.export thy (Path.implode prv_path)
     1.8 +            Export.export thy prv_path
     1.9                [implode (map (fn (s, _) => snd (strip_number s) ^
    1.10                  " -- proved by " ^ Distribution.version ^ "\n") proved'')];
    1.11          in {pfuns = pfuns, type_map = type_map, env = NONE} end))
     2.1 --- a/src/Pure/General/path.ML	Sat Feb 02 14:51:11 2019 +0100
     2.2 +++ b/src/Pure/General/path.ML	Sat Feb 02 15:52:14 2019 +0100
     2.3 @@ -7,7 +7,6 @@
     2.4  
     2.5  signature PATH =
     2.6  sig
     2.7 -  val check_elem: string -> unit
     2.8    eqtype T
     2.9    val is_current: T -> bool
    2.10    val current: T
    2.11 @@ -20,6 +19,7 @@
    2.12    val has_parent: T -> bool
    2.13    val is_absolute: T -> bool
    2.14    val is_basic: T -> bool
    2.15 +  val all_basic: T -> bool
    2.16    val starts_basic: T -> bool
    2.17    val append: T -> T -> T
    2.18    val appends: T list -> T
    2.19 @@ -57,8 +57,6 @@
    2.20  val illegal_elem = ["", "~", "~~", ".", ".."];
    2.21  val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"];
    2.22  
    2.23 -in
    2.24 -
    2.25  fun check_elem s =
    2.26    if member (op =) illegal_elem s then err_elem "Illegal" s
    2.27    else
    2.28 @@ -69,6 +67,8 @@
    2.29          err_elem ("Illegal character " ^ quote c ^ " in") s
    2.30        else ());
    2.31  
    2.32 +in
    2.33 +
    2.34  val root_elem = Root o tap check_elem;
    2.35  val basic_elem = Basic o tap check_elem;
    2.36  val variable_elem = Variable o tap check_elem;
    2.37 @@ -103,6 +103,9 @@
    2.38  fun is_basic (Path [Basic _]) = true
    2.39    | is_basic _ = false;
    2.40  
    2.41 +fun all_basic (Path elems) =
    2.42 +  forall (fn Basic _ => true | _ => false) elems;
    2.43 +
    2.44  fun starts_basic (Path xs) =
    2.45    (case try List.last xs of
    2.46      SOME (Basic _) => true
     3.1 --- a/src/Pure/Thy/export.ML	Sat Feb 02 14:51:11 2019 +0100
     3.2 +++ b/src/Pure/Thy/export.ML	Sat Feb 02 15:52:14 2019 +0100
     3.3 @@ -6,8 +6,8 @@
     3.4  
     3.5  signature EXPORT =
     3.6  sig
     3.7 -  val export: theory -> string -> string list -> unit
     3.8 -  val export_raw: theory -> string -> string list -> unit
     3.9 +  val export: theory -> Path.T -> string list -> unit
    3.10 +  val export_raw: theory -> Path.T -> string list -> unit
    3.11    val markup: theory -> string -> Markup.T
    3.12    val message: theory -> string -> string
    3.13  end;
    3.14 @@ -17,20 +17,20 @@
    3.15  
    3.16  (* export *)
    3.17  
    3.18 -fun check_name name =
    3.19 +fun check_name path =
    3.20    let
    3.21 +    val name = Path.implode path;
    3.22      val _ =
    3.23 -      (case space_explode "/" name of
    3.24 -        [] => error "Empty export name"
    3.25 -      | elems => List.app Path.check_elem elems);
    3.26 +      if not (Path.is_current path) andalso Path.all_basic path then ()
    3.27 +      else error ("Bad export name: " ^ quote name);
    3.28    in name end;
    3.29  
    3.30 -fun gen_export compress thy name body =
    3.31 +fun gen_export compress thy path body =
    3.32    (Output.try_protocol_message o Markup.export)
    3.33     {id = Position.get_id (Position.thread_data ()),
    3.34      serial = serial (),
    3.35      theory_name = Context.theory_long_name thy,
    3.36 -    name = check_name name,
    3.37 +    name = check_name path,
    3.38      compress = compress} body;
    3.39  
    3.40  val export = gen_export true;
     4.1 --- a/src/Pure/Thy/export_theory.ML	Sat Feb 02 14:51:11 2019 +0100
     4.2 +++ b/src/Pure/Thy/export_theory.ML	Sat Feb 02 15:52:14 2019 +0100
     4.3 @@ -161,7 +161,8 @@
     4.4      if Options.bool (#options context) "export_theory" then f context thy else ()));
     4.5  
     4.6  fun export_body thy name body =
     4.7 -  Export.export thy ("theory/" ^ name) (Buffer.chunks (YXML.buffer_body body Buffer.empty));
     4.8 +  Export.export thy (Path.make ["theory", name])
     4.9 +    (Buffer.chunks (YXML.buffer_body body Buffer.empty));
    4.10  
    4.11  
    4.12  (* presentation *)
     5.1 --- a/src/Pure/Thy/thy_info.ML	Sat Feb 02 14:51:11 2019 +0100
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Feb 02 15:52:14 2019 +0100
     5.3 @@ -66,7 +66,7 @@
     5.4              val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
     5.5              val _ =
     5.6                if Options.bool options "export_document"
     5.7 -              then Export.export thy "document.tex" output else ();
     5.8 +              then Export.export thy (Path.explode "document.tex") output else ();
     5.9              val _ = if #enabled option then Present.theory_output thy output else ();
    5.10            in () end
    5.11        end));
     6.1 --- a/src/Pure/Tools/generated_files.ML	Sat Feb 02 14:51:11 2019 +0100
     6.2 +++ b/src/Pure/Tools/generated_files.ML	Sat Feb 02 15:52:14 2019 +0100
     6.3 @@ -81,7 +81,7 @@
     6.4  fun export_files thy other_thys =
     6.5    other_thys |> maps (fn other_thy =>
     6.6      get_files other_thy |> map (fn {path, pos, text} =>
     6.7 -      (Export.export thy (Path.implode path) [text]; (path, pos))));
     6.8 +      (Export.export thy path [text]; (path, pos))));
     6.9  
    6.10  
    6.11  (* file types *)
     7.1 --- a/src/Tools/Code/code_target.ML	Sat Feb 02 14:51:11 2019 +0100
     7.2 +++ b/src/Tools/Code/code_target.ML	Sat Feb 02 15:52:14 2019 +0100
     7.3 @@ -180,9 +180,10 @@
     7.4    (Export.export thy name [content]; writeln (Export.message thy ""));
     7.5  
     7.6  fun export_to_exports thy width (Singleton (extension, p)) =
     7.7 -      export_information thy (generatedN ^ "." ^ extension) (Code_Printer.format [] width p)
     7.8 +      export_information thy (Path.basic (generatedN ^ "." ^ extension))
     7.9 +        (Code_Printer.format [] width p)
    7.10    | export_to_exports thy width (Hierarchy code_modules) = (
    7.11 -      map (fn (names, p) => export_information thy (Path.implode (Path.make names))
    7.12 +      map (fn (names, p) => export_information thy (Path.make names)
    7.13          (Code_Printer.format [] width p)) code_modules;
    7.14        ());
    7.15