--- a/src/Pure/Pure.thy Sat Dec 01 15:55:04 2018 +0100
+++ b/src/Pure/Pure.thy Sat Dec 01 16:11:59 2018 +0100
@@ -123,7 +123,7 @@
Outer_Syntax.local_theory \<^command_keyword>\<open>generate_file\<close>
"generate source file, with antiquotations"
(Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
- >> Generate_File.generate_file_cmd);
+ >> Generated_Files.generate_file_cmd);
in end\<close>
--- a/src/Pure/ROOT.ML Sat Dec 01 15:55:04 2018 +0100
+++ b/src/Pure/ROOT.ML Sat Dec 01 16:11:59 2018 +0100
@@ -347,4 +347,4 @@
ML_file "Tools/named_theorems.ML";
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
-ML_file "Tools/generate_file.ML"
+ML_file "Tools/generated_files.ML"
--- a/src/Pure/Tools/generate_file.ML Sat Dec 01 15:55:04 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,218 +0,0 @@
-(* Title: Pure/Tools/generate_file.ML
- Author: Makarius
-
-Generate source files for other languages (with antiquotations, without Isabelle symbols).
-*)
-
-signature GENERATE_FILE =
-sig
- type file_type =
- {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
- val file_type:
- binding -> {ext: string, make_comment: string -> string, make_string: string -> string} ->
- theory -> theory
- val antiquotation: binding -> 'a Token.context_parser ->
- ({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) ->
- theory -> theory
- val set_string: string -> Proof.context -> Proof.context
- val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory
- val generate: theory -> Path.T -> Path.T list
-end;
-
-structure Generate_File: GENERATE_FILE =
-struct
-
-(** context data **)
-
-type file_type =
- {name: string, ext: string, make_comment: string -> string, make_string: string -> string};
-
-type antiquotation = Token.src -> Proof.context -> file_type -> string;
-
-structure Data = Theory_Data
-(
- type T =
- file_type Name_Space.table * (*file types*)
- antiquotation Name_Space.table * (*antiquotations*)
- (Path.T * (Position.T * string)) list; (*generated files for current theory*)
- val empty =
- (Name_Space.empty_table Markup.file_typeN,
- Name_Space.empty_table Markup.antiquotationN,
- []);
- val extend = @{apply 3(3)} (K []);
- fun merge ((types1, antiqs1, _), (types2, antiqs2, _)) =
- (Name_Space.merge_tables (types1, types2),
- Name_Space.merge_tables (antiqs1, antiqs2),
- []);
-);
-
-val get_files = rev o #3 o Data.get;
-
-fun add_files (path, (pos, text)) =
- (Data.map o @{apply 3(3)}) (fn files =>
- (case AList.lookup (op =) files path of
- SOME (pos', _) =>
- error ("Duplicate generated file " ^ Path.print path ^ Position.here_list [pos, pos'])
- | NONE => (path, (pos, text)) :: files));
-
-
-(* file types *)
-
-fun the_file_type thy ext =
- if ext = "" then error "Bad file extension"
- else
- (#1 (Data.get thy), NONE) |-> Name_Space.fold_table
- (fn (_, file_type) => fn res =>
- if #ext file_type = ext then SOME file_type else res)
- |> (fn SOME file_type => file_type
- | NONE => error ("Unknown file type for extension " ^ quote ext));
-
-fun file_type binding {ext, make_comment, make_string} thy =
- let
- val name = Binding.name_of binding;
- val pos = Binding.pos_of binding;
- val file_type = {name = name, ext = ext, make_comment = make_comment, make_string = make_string};
-
- val table = #1 (Data.get thy);
- val space = Name_Space.space_of_table table;
- val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming);
- val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type);
-
- val _ =
- (case try (#name o the_file_type thy) ext of
- NONE => ()
- | SOME name' =>
- error ("Extension " ^ quote ext ^ " already registered for file type " ^
- quote (Markup.markup (Name_Space.markup space name') name') ^ Position.here pos));
- in thy |> (Data.map o @{apply 3(1)}) (K data') end;
-
-
-(* antiquotations *)
-
-val get_antiquotations = #2 o Data.get o Proof_Context.theory_of;
-
-fun antiquotation name scan body thy =
- let
- fun ant src ctxt file_type : string =
- let val (x, ctxt') = Token.syntax scan src ctxt
- in body {context = ctxt', source = src, file_type = file_type, argument = x} end;
- in
- thy
- |> (Data.map o @{apply 3(2)}) (Name_Space.define (Context.Theory thy) true (name, ant) #> #2)
- end;
-
-val scan_antiq =
- Antiquote.scan_control >> Antiquote.Control ||
- Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
-
-fun read_source ctxt (file_type: file_type) source =
- let
- val _ =
- Context_Position.report ctxt (Input.pos_of source)
- (Markup.language
- {name = #name file_type, symbols = false, antiquotes = true,
- delimited = Input.is_delimited source});
-
- val (input, _) =
- Input.source_explode source
- |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq));
-
- val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input);
-
- fun expand antiq =
- (case antiq of
- Antiquote.Text s => s
- | Antiquote.Control {name, body, ...} =>
- let
- val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]);
- val (src', ant) = Token.check_src ctxt get_antiquotations src;
- in ant src' ctxt file_type end
- | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq))));
- in implode (map expand input) end;
-
-
-(* generate files *)
-
-fun generate_file_cmd ((file, pos), source) lthy =
- let
- val thy = Proof_Context.theory_of lthy;
-
- val path = Path.expand (Path.explode file);
- fun err_path msg = error (msg ^ ": " ^ Path.print path ^ Position.here pos);
- val _ =
- if Path.is_absolute path then err_path "Illegal absolute path"
- else if Path.has_parent path then err_path "Illegal parent path"
- else ();
-
- 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 text = header ^ "\n" ^ read_source lthy file_type source;
- in lthy |> (Local_Theory.background_theory o add_files) (path, (pos, text)) end;
-
-fun generate thy dir =
- thy |> get_files |> List.map (fn (path, (_, text)) =>
- let
- val path' = Path.expand (Path.append dir path);
- val _ = Isabelle_System.mkdirs (Path.dir path');
- val _ = File.generate path' text;
- in path end);
-
-
-
-(** concrete file types **)
-
-val _ =
- Theory.setup
- (file_type \<^binding>\<open>Haskell\<close>
- {ext = "hs",
- make_comment = enclose "{-" "-}",
- make_string = GHC.print_string});
-
-
-
-(** concrete antiquotations **)
-
-(* ML expression as string literal *)
-
-structure Local_Data = Proof_Data
-(
- type T = string option;
- fun init _ = NONE;
-);
-
-val set_string = Local_Data.put o SOME;
-
-fun the_string ctxt =
- (case Local_Data.get ctxt of
- SOME s => s
- | NONE => raise Fail "No result string");
-
-val _ =
- Theory.setup
- (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
- (fn {context = ctxt, file_type, argument, ...} =>
- ctxt |> Context.proof_map
- (ML_Context.expression (Input.pos_of argument)
- (ML_Lex.read "Theory.local_setup (Generate_File.set_string (" @
- ML_Lex.read_source argument @ ML_Lex.read "))"))
- |> the_string |> #make_string file_type));
-
-
-(* file-system paths *)
-
-fun path_antiquotation binding check =
- antiquotation binding
- (Args.context -- Scan.lift (Parse.position Parse.path) >>
- (fn (ctxt, (name, pos)) => (check ctxt Path.current (name, pos) |> Path.implode)))
- (fn {file_type, argument, ...} => #make_string file_type argument);
-
-val _ =
- Theory.setup
- (path_antiquotation \<^binding>\<open>path\<close> Resources.check_path #>
- path_antiquotation \<^binding>\<open>file\<close> Resources.check_file #>
- path_antiquotation \<^binding>\<open>dir\<close> Resources.check_dir);
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/generated_files.ML Sat Dec 01 16:11:59 2018 +0100
@@ -0,0 +1,226 @@
+(* Title: Pure/Tools/generated_files.ML
+ Author: Makarius
+
+Generated source files for other languages: with antiquotations, without Isabelle symbols.
+*)
+
+signature GENERATED_FILES =
+sig
+ type file_type =
+ {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
+ val file_type:
+ binding -> {ext: string, make_comment: string -> string, make_string: string -> string} ->
+ theory -> theory
+ val antiquotation: binding -> 'a Token.context_parser ->
+ ({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) ->
+ theory -> theory
+ val set_string: string -> Proof.context -> Proof.context
+ val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory
+ val write: theory -> Path.T -> Path.T list
+ val export: theory -> string -> Path.T list
+end;
+
+structure Generated_Files: GENERATED_FILES =
+struct
+
+(** context data **)
+
+type file_type =
+ {name: string, ext: string, make_comment: string -> string, make_string: string -> string};
+
+type antiquotation = Token.src -> Proof.context -> file_type -> string;
+
+structure Data = Theory_Data
+(
+ type T =
+ file_type Name_Space.table * (*file types*)
+ antiquotation Name_Space.table * (*antiquotations*)
+ (Path.T * (Position.T * string)) list; (*generated files for current theory*)
+ val empty =
+ (Name_Space.empty_table Markup.file_typeN,
+ Name_Space.empty_table Markup.antiquotationN,
+ []);
+ val extend = @{apply 3(3)} (K []);
+ fun merge ((types1, antiqs1, _), (types2, antiqs2, _)) =
+ (Name_Space.merge_tables (types1, types2),
+ Name_Space.merge_tables (antiqs1, antiqs2),
+ []);
+);
+
+val get_files = rev o #3 o Data.get;
+
+fun add_files (path, (pos, text)) =
+ (Data.map o @{apply 3(3)}) (fn files =>
+ (case AList.lookup (op =) files path of
+ SOME (pos', _) =>
+ error ("Duplicate generated file " ^ Path.print path ^ Position.here_list [pos, pos'])
+ | NONE => (path, (pos, text)) :: files));
+
+
+(* file types *)
+
+fun the_file_type thy ext =
+ if ext = "" then error "Bad file extension"
+ else
+ (#1 (Data.get thy), NONE) |-> Name_Space.fold_table
+ (fn (_, file_type) => fn res =>
+ if #ext file_type = ext then SOME file_type else res)
+ |> (fn SOME file_type => file_type
+ | NONE => error ("Unknown file type for extension " ^ quote ext));
+
+fun file_type binding {ext, make_comment, make_string} thy =
+ let
+ val name = Binding.name_of binding;
+ val pos = Binding.pos_of binding;
+ val file_type = {name = name, ext = ext, make_comment = make_comment, make_string = make_string};
+
+ val table = #1 (Data.get thy);
+ val space = Name_Space.space_of_table table;
+ val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming);
+ val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type);
+
+ val _ =
+ (case try (#name o the_file_type thy) ext of
+ NONE => ()
+ | SOME name' =>
+ error ("Extension " ^ quote ext ^ " already registered for file type " ^
+ quote (Markup.markup (Name_Space.markup space name') name') ^ Position.here pos));
+ in thy |> (Data.map o @{apply 3(1)}) (K data') end;
+
+
+(* antiquotations *)
+
+val get_antiquotations = #2 o Data.get o Proof_Context.theory_of;
+
+fun antiquotation name scan body thy =
+ let
+ fun ant src ctxt file_type : string =
+ let val (x, ctxt') = Token.syntax scan src ctxt
+ in body {context = ctxt', source = src, file_type = file_type, argument = x} end;
+ in
+ thy
+ |> (Data.map o @{apply 3(2)}) (Name_Space.define (Context.Theory thy) true (name, ant) #> #2)
+ end;
+
+val scan_antiq =
+ Antiquote.scan_control >> Antiquote.Control ||
+ Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
+
+fun read_source ctxt (file_type: file_type) source =
+ let
+ val _ =
+ Context_Position.report ctxt (Input.pos_of source)
+ (Markup.language
+ {name = #name file_type, symbols = false, antiquotes = true,
+ delimited = Input.is_delimited source});
+
+ val (input, _) =
+ Input.source_explode source
+ |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq));
+
+ val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input);
+
+ fun expand antiq =
+ (case antiq of
+ Antiquote.Text s => s
+ | Antiquote.Control {name, body, ...} =>
+ let
+ val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]);
+ val (src', ant) = Token.check_src ctxt get_antiquotations src;
+ in ant src' ctxt file_type end
+ | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq))));
+ in implode (map expand input) end;
+
+
+(* generate files *)
+
+fun generate_file_cmd ((file, pos), source) lthy =
+ let
+ val thy = Proof_Context.theory_of lthy;
+
+ val path = Path.expand (Path.explode file);
+ fun err_path msg = error (msg ^ ": " ^ Path.print path ^ Position.here pos);
+ val _ =
+ if Path.is_absolute path then err_path "Illegal absolute path"
+ else if Path.has_parent path then err_path "Illegal parent path"
+ else ();
+
+ 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 text = header ^ "\n" ^ read_source lthy file_type source;
+ in lthy |> (Local_Theory.background_theory o add_files) (path, (pos, text)) end;
+
+fun write thy dir =
+ get_files thy |> map (fn (path, (_, text)) =>
+ let
+ val path' = Path.expand (Path.append dir path);
+ val _ = Isabelle_System.mkdirs (Path.dir path');
+ val _ = File.generate path' text;
+ in path end);
+
+fun export thy prefix =
+ get_files thy |> map (fn (path, (_, text)) =>
+ let
+ val name = (if prefix = "" then "" else prefix ^ "/") ^ Path.implode path;
+ val _ = Export.export thy name [text];
+ in path end);
+
+
+
+(** concrete file types **)
+
+val _ =
+ Theory.setup
+ (file_type \<^binding>\<open>Haskell\<close>
+ {ext = "hs",
+ make_comment = enclose "{-" "-}",
+ make_string = GHC.print_string});
+
+
+
+(** concrete antiquotations **)
+
+(* ML expression as string literal *)
+
+structure Local_Data = Proof_Data
+(
+ type T = string option;
+ fun init _ = NONE;
+);
+
+val set_string = Local_Data.put o SOME;
+
+fun the_string ctxt =
+ (case Local_Data.get ctxt of
+ SOME s => s
+ | NONE => raise Fail "No result string");
+
+val _ =
+ Theory.setup
+ (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
+ (fn {context = ctxt, file_type, argument, ...} =>
+ ctxt |> Context.proof_map
+ (ML_Context.expression (Input.pos_of argument)
+ (ML_Lex.read "Theory.local_setup (Generated_Files.set_string (" @
+ ML_Lex.read_source argument @ ML_Lex.read "))"))
+ |> the_string |> #make_string file_type));
+
+
+(* file-system paths *)
+
+fun path_antiquotation binding check =
+ antiquotation binding
+ (Args.context -- Scan.lift (Parse.position Parse.path) >>
+ (fn (ctxt, (name, pos)) => (check ctxt Path.current (name, pos) |> Path.implode)))
+ (fn {file_type, argument, ...} => #make_string file_type argument);
+
+val _ =
+ Theory.setup
+ (path_antiquotation \<^binding>\<open>path\<close> Resources.check_path #>
+ path_antiquotation \<^binding>\<open>file\<close> Resources.check_file #>
+ path_antiquotation \<^binding>\<open>dir\<close> Resources.check_dir);
+
+end;
--- a/src/Tools/Haskell/Test.thy Sat Dec 01 15:55:04 2018 +0100
+++ b/src/Tools/Haskell/Test.thy Sat Dec 01 16:11:59 2018 +0100
@@ -10,7 +10,7 @@
ML \<open>
Isabelle_System.with_tmp_dir "ghc" (fn dir =>
let
- val files = Generate_File.generate \<^theory>\<open>Haskell\<close> dir;
+ val files = Generated_Files.write \<^theory>\<open>Haskell\<close> dir;
val (out, rc) =
Isabelle_System.bash_output
(cat_lines