From cbb96cf3c3965e78a480ad65a41da67041dcd7fc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?=
<tuong@users.noreply.github.com>
Date: Sat, 25 Dec 2021 19:53:52 -0800
Subject: [PATCH] upgrade to Isabelle2021
---
Citadelle/ROOT | 10 ++-
.../compiler/Generator_dynamic_sequential.thy | 86 +++++++++++--------
.../Generator_dynamic_concurrent.thy | 86 +++++++++++--------
.../Generator_dynamic_export_testing.thy | 60 +++++++------
.../ex/C_Model_ex_hol.thy | 16 +++-
.../ex/C_Model_ex_meta.thy | 17 +++-
.../Generator_dynamic_sequential.thy | 23 ++---
.../src/compiler_misc/meta/Printer_init.thy | 40 +++++----
8 files changed, 203 insertions(+), 135 deletions(-)
diff --git a/Citadelle/ROOT b/Citadelle/ROOT
index 7ba6561940f..987c9f7a76e 100644
--- a/Citadelle/ROOT
+++ b/Citadelle/ROOT
@@ -122,14 +122,22 @@ session "Citadelle_C_deep-dirty" in "src/compiler_citadelle_c/doc" = Citadelle_C
session "Citadelle_C_shallow-dirty" in "src/compiler_citadelle_c/core" = Citadelle_C_init +
options [quick_and_dirty]
+ directories
+ "$HASKABELLE_HOME_USER/default"
theories
C_Model_core
-session "Citadelle_C_model-dirty" in "src/compiler_citadelle_c/ml" = "Citadelle_C_shallow-dirty" +
+session "Citadelle_C_ml-dirty" in "src/compiler_citadelle_c/ml" = "Citadelle_C_shallow-dirty" +
options [quick_and_dirty]
theories
C_Model_ml
+session "Citadelle_C_ex-dirty" in "src/compiler_citadelle_c/ex" = "Citadelle_C_shallow-dirty" +
+ options [quick_and_dirty]
+ theories
+ C_Model_ex_hol
+ C_Model_ex_meta
+
(******************************************************)
session "Max-dirty" = "HOL-Library" (* Note: replacing with FOCL will fail! *) +
diff --git a/Citadelle/src/compiler/Generator_dynamic_sequential.thy b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
index 07a9fe035e7..704034f5175 100644
--- a/Citadelle/src/compiler/Generator_dynamic_sequential.thy
+++ b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
@@ -209,23 +209,28 @@ structure Outer_Syntax' = struct
end
structure Resources' = struct
- fun check_path' check_file ctxt dir (name, pos) =
+ fun formal_check check_file ctxt opt_dir source =
let
- fun err msg pos = error (msg ^ Position.here pos)
- val _ = Context_Position.report ctxt pos Markup.language_path;
+ val name = Input.string_of source;
+ val pos = Input.pos_of source;
+ val delimited = Input.is_delimited source;
- val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
- val path' = Path.expand path handle ERROR msg => err msg pos;
- val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
- val _ =
- (case check_file of
- NONE => path
- | SOME check => (check path handle ERROR msg => err msg pos));
- in Path.implode path' end
-
- fun check_dir thy = check_path' (SOME File.check_dir)
- (Proof_Context.init_global thy)
- (Resources.master_directory thy)
+ val _ = Context_Position.report ctxt pos (Markup.language_path delimited);
+
+ fun err msg = error (msg ^ Position.here pos);
+ val dir =
+ (case opt_dir of
+ SOME dir => dir
+ | NONE => Resources.master_directory (Proof_Context.theory_of ctxt));
+ val path = dir + Path.explode name handle ERROR msg => err msg;
+ val path' = Path.implode_symbolic path;
+ val _ = Path.expand path handle ERROR msg => err msg;
+ val _ = Context_Position.report ctxt pos (Markup.path path');
+ val _ : Path.T = check_file path handle ERROR msg => err msg;
+ in path' end;
+
+ val check_file = formal_check File.check_file;
+ val check_dir = formal_check File.check_dir;
end
\<close>
@@ -266,7 +271,7 @@ type ('transitionM, 'Proof_stateM, 'state) toplevel =
, keep: ('state -> unit) -> 'transitionM
, generic_theory: (generic_theory -> generic_theory) -> 'transitionM
, theory: (theory -> theory) -> 'transitionM
- , begin_local_theory: bool -> (theory -> local_theory) -> 'transitionM
+ , begin_main_target: bool -> (theory -> local_theory) -> 'transitionM
, local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
(bool -> local_theory -> local_theory) -> 'transitionM
, local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
@@ -468,7 +473,7 @@ fun semi__command_proof top = let open META_overload
end
fun end' top =
- (\<^command_keyword>\<open>end\<close>, #tr_raw top (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
+ (\<^command_keyword>\<open>end\<close>, #tr_raw top (Toplevel.exit o Toplevel.end_main_target o Toplevel.end_nested_target o
Toplevel.end_proof (K Proof.end_notepad)))
structure Cmd = struct open META open META_overload
@@ -630,13 +635,13 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
| Theory_type_notation type_notation =>
cons (\<^command_keyword>\<open>type_notation\<close>, Cmd.type_notation top type_notation)
| Theory_instantiation (Instantiation (n, n_def, expr)) => let val name = To_string0 n in fn acc => acc
- |>:: (\<^command_keyword>\<open>instantiation\<close>, #begin_local_theory top true (Cmd.instantiation1 name))
+ |>:: (\<^command_keyword>\<open>instantiation\<close>, #begin_main_target top true (Cmd.instantiation1 name))
|>:: (\<^command_keyword>\<open>definition\<close>, #local_theory' top NONE NONE (#2 oo Cmd.instantiation2 name n_def expr))
|>:: (\<^command_keyword>\<open>instance\<close>, #local_theory_to_proof top NONE NONE (Class.instantiation_instance I))
|>:: (\<^command_keyword>\<open>..\<close>, #tr_raw top Isar_Cmd.default_proof)
|>:: end' top end
| Theory_overloading (Overloading (n_c, e_c, n, e)) => (fn acc => acc
- |>:: (\<^command_keyword>\<open>overloading\<close>, #begin_local_theory top true (Cmd.overloading1 n_c e_c))
+ |>:: (\<^command_keyword>\<open>overloading\<close>, #begin_main_target top true (Cmd.overloading1 n_c e_c))
|>:: (\<^command_keyword>\<open>definition\<close>, #local_theory' top NONE NONE (Cmd.overloading2 n e))
|>:: end' top)
| Theory_consts consts =>
@@ -807,6 +812,7 @@ local
|> ( Expression.add_locale_cmd
(To_sbinding (META.holThyLocale_name data))
Binding.empty
+ []
([], [])
(List.concat
(map
@@ -853,7 +859,7 @@ fun all_meta_tr aux top thy_o = fn
(case theo of
Theories_one theo => Command_Transition.semi__theory top theo
| Theories_locale (data, l) => fn acc => acc
- |>:: (\<^command_keyword>\<open>locale\<close>, #begin_local_theory top true (semi__locale data))
+ |>:: (\<^command_keyword>\<open>locale\<close>, #begin_main_target top true (semi__locale data))
|> fold (fold (Command_Transition.semi__theory top)) l
|>:: end' top)
| META_boot_generation_syntax _ => I
@@ -882,7 +888,7 @@ fun all_meta_thy aux top_theory top_local_theory = fn
META_semi_theories theo => apsnd
(case theo of
Theories_one theo => Command_Theory.semi__theory top_theory theo
- | Theories_locale (data, l) => (*Toplevel.begin_local_theory*) fn thy => thy
+ | Theories_locale (data, l) => (*Toplevel.begin_main_target*) fn thy => thy
|> semi__locale data
|> fold (fold (Command_Theory.semi__theory top_local_theory)) l
|> Local_Theory.exit_global)
@@ -1222,12 +1228,12 @@ fun thy_shallow l_obj get_all_meta_embed =
(fn msg =>
let val () = disp_time msg ()
fun in_self f =
- \<comment> \<open>Note: This function is not equivalent to \<^ML>\<open>Local_Theory.subtarget\<close>.\<close>
+ \<comment> \<open>Note: This function is not equivalent to \<^ML>\<open>Local_Theory.begin_nested\<close> \<^ML>\<open>Local_Theory.end_nested\<close>.\<close>
Local_Theory.new_group
#> f
#> Local_Theory.reset_group
#> (fn lthy =>
- #1 (Named_Target.switch NONE (Context.Proof lthy)) lthy |> Context.the_proof)
+ #1 (Target_Context.switch_named_cmd NONE (Context.Proof lthy)) lthy |> Context.the_proof)
fun not_used p _ = error ("not used " ^ Position.here p)
val context_of = I
fun proof' f = f true
@@ -1248,7 +1254,7 @@ fun thy_shallow l_obj get_all_meta_embed =
, tr_report = report, tr_report_o = report_o
, pr_report = report, pr_report_o = report_o
(* irrelevant part *)
- , begin_local_theory = K o not_used \<^here>
+ , begin_main_target = K o not_used \<^here>
, local_theory_to_proof' = K o K not_used \<^here>
, local_theory_to_proof = K o K not_used \<^here>
, tr_raw = not_used \<^here> }
@@ -1265,7 +1271,7 @@ fun thy_shallow l_obj get_all_meta_embed =
, tr_report = report, tr_report_o = report_o
, pr_report = report, pr_report_o = report_o
(* irrelevant part *)
- , begin_local_theory = K o not_used \<^here>
+ , begin_main_target = K o not_used \<^here>
, local_theory_to_proof' = K o K not_used \<^here>
, local_theory_to_proof = K o K not_used \<^here>
, tr_raw = not_used \<^here> }
@@ -1353,7 +1359,7 @@ fun outer_syntax_commands'''' is_safe mk_string get_all_meta_embed name thy _ =
, keep = Toplevel.keep
, generic_theory = Toplevel.generic_theory
, theory = Toplevel.theory
- , begin_local_theory = Toplevel.begin_local_theory
+ , begin_main_target = Toplevel.begin_main_target
, local_theory' = Toplevel.local_theory'
, local_theory = Toplevel.local_theory
, local_theory_to_proof' = Toplevel.local_theory_to_proof'
@@ -1715,7 +1721,7 @@ structure USE_parse = struct
-- optional_b \<^keyword>\<open>ignore_not_in_scope\<close>
-- optional_b \<^keyword>\<open>abstract_mutual_data_params\<close>
-- optional_b \<^keyword>\<open>concat_modules\<close>
- -- Scan.option (\<^keyword>\<open>base_path\<close> |-- Parse.position Parse.path)
+ -- Scan.option (\<^keyword>\<open>base_path\<close> |-- Parse.path_input)
-- Scan.optional (parse_l' (Parse.name -- Scan.option ((\<^keyword>\<open>\<rightharpoonup>\<close> || \<^keyword>\<open>=>\<close>) |-- Parse.name))) []
end
\<close>
@@ -1951,7 +1957,7 @@ local
val haskabelle_bin = haskabelle_path "HASKABELLE_HOME" ["bin", "haskabelle_bin"]
val haskabelle_default = haskabelle_path "HASKABELLE_HOME_USER" ["default"]
in
- fun parse meta_parse_shallow meta_parse_imports meta_parse_code meta_parse_functions hsk_name check_dir hsk_str ((((((((old_datatype, try_import), only_types), ignore_not_in_scope), abstract_mutual_data_params), concat_modules), base_path_abs), l_rewrite), (content, pos)) thy =
+ fun parse meta_parse_shallow meta_parse_imports meta_parse_code meta_parse_functions hsk_name check_dir hsk_str ((((((((old_datatype, try_import), only_types), ignore_not_in_scope), abstract_mutual_data_params), concat_modules), base_path_abs), l_rewrite), source) thy =
let fun string_of_bool b = if b then "true" else "false"
val st =
Bash.process
@@ -1961,7 +1967,7 @@ in
, "--export", "false"
, "--try-import", string_of_bool try_import
, "--only-types", string_of_bool only_types
- , "--base-path-abs", case base_path_abs of NONE => "" | SOME s => check_dir thy s
+ , "--base-path-abs", case base_path_abs of NONE => "" | SOME source => check_dir (Proof_Context.init_global thy) NONE source
, "--ignore-not-in-scope", string_of_bool ignore_not_in_scope
, "--abstract-mutual-data-params", string_of_bool abstract_mutual_data_params
, "--dump-output"
@@ -1972,9 +1978,9 @@ in
[ "--hsk-name" ] @ the_list hsk_name
@ (case
if hsk_str then
- ([ Bash.string content ], [])
+ ([ Bash.string (Input.string_of source) ], [])
else
- ([], [ Resources'.check_path' (SOME File.check_file) (Proof_Context.init_global thy) Path.current (content, pos) ])
+ ([], [ Resources'.check_file (Proof_Context.init_global thy) (SOME Path.current) source ])
of (cts, files) => List.concat [ ["--hsk-contents"], cts, ["--files"], files ])))
in
if #rc st = 0 then
@@ -2001,7 +2007,7 @@ in
:: acc)
end)
l_rep
- (Symbol.explode content, (Position.advance_offsets 1 pos, 0), [])
+ (Symbol.explode (Input.string_of source), (Position.advance_offsets 1 (Input.pos_of source), 0), [])
|> #3
in Position.reports l_rep end)
l_rep
@@ -2023,7 +2029,7 @@ end
local
type haskell_parse =
- (((((((bool * Code_Numeral.natural) * bool) * bool) * bool) * bool) * bool) * (string * Position.T) option)
+ (((((((bool * Code_Numeral.natural) * bool) * bool) * bool) * bool) * bool) * Input.source option)
* (string * string option) list
structure Data_lang = Theory_Data
@@ -2032,16 +2038,20 @@ local
val extend = I
val merge = Name_Space.merge_tables)
+ structure Parse' =
+ struct
+ val haskell_source = Parse.input (Parse.group (fn () => "Haskell source") Parse.text)
+ end
open USE_parse
in
val () =
outer_syntax_commands'2 \<^mk_string> \<^command_keyword>\<open>Haskell\<close> ""
- (haskell_parse -- Parse.position Parse.cartouche)
+ (haskell_parse -- Parse'.haskell_source)
(get_thy \<^here> o parse' true)
val () =
outer_syntax_commands'2 \<^mk_string> \<^command_keyword>\<open>Haskell_file\<close> ""
- (haskell_parse -- Parse.position Parse.path)
+ (haskell_parse -- Parse.path_input)
(get_thy \<^here> o parse' false)
val () =
@@ -2074,14 +2084,14 @@ val () =
(#2 o Name_Space.define
(Context.Theory thy)
true
- (lang, (hsk_arg, Option.map (Resources'.check_dir thy) base_path, imports, defines, functions)))
+ (lang, (hsk_arg, Option.map (Resources'.check_dir (Proof_Context.init_global thy) NONE) base_path, imports, defines, functions)))
thy)
end))
val () =
outer_syntax_commands'2 \<^mk_string> \<^command_keyword>\<open>language\<close> ""
(Scan.optional (\<^keyword>\<open>meta\<close> >> K true) false
- -- Parse.binding --| Parse.$$$ "::" -- Parse.position Parse.name --| Parse.where_ -- Parse.position Parse.cartouche)
+ -- Parse.binding --| Parse.$$$ "::" -- Parse.position Parse.name --| Parse.where_ -- Parse'.haskell_source)
(fn (((is_shallow, prog), lang), code) =>
get_thy \<^here>
(fn thy =>
@@ -2093,7 +2103,7 @@ val () =
(SOME defines)
(functions (From.string prog'))
(SOME prog')
- (K (K (case hsk_path of NONE => "" | SOME s => s)))
+ (K (K (K (case hsk_path of NONE => "" | SOME s => s))))
true
(hsk_arg, code)
thy
diff --git a/Citadelle/src/compiler_citadelle/Generator_dynamic_concurrent.thy b/Citadelle/src/compiler_citadelle/Generator_dynamic_concurrent.thy
index 37120a1c1af..641ae8e8f65 100644
--- a/Citadelle/src/compiler_citadelle/Generator_dynamic_concurrent.thy
+++ b/Citadelle/src/compiler_citadelle/Generator_dynamic_concurrent.thy
@@ -187,23 +187,28 @@ structure Toplevel' = struct
end
structure Resources' = struct
- fun check_path' check_file ctxt dir (name, pos) =
+ fun formal_check check_file ctxt opt_dir source =
let
- fun err msg pos = error (msg ^ Position.here pos)
- val _ = Context_Position.report ctxt pos Markup.language_path;
+ val name = Input.string_of source;
+ val pos = Input.pos_of source;
+ val delimited = Input.is_delimited source;
- val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
- val path' = Path.expand path handle ERROR msg => err msg pos;
- val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
- val _ =
- (case check_file of
- NONE => path
- | SOME check => (check path handle ERROR msg => err msg pos));
- in Path.implode path' end
-
- fun check_dir thy = check_path' (SOME File.check_dir)
- (Proof_Context.init_global thy)
- (Resources.master_directory thy)
+ val _ = Context_Position.report ctxt pos (Markup.language_path delimited);
+
+ fun err msg = error (msg ^ Position.here pos);
+ val dir =
+ (case opt_dir of
+ SOME dir => dir
+ | NONE => Resources.master_directory (Proof_Context.theory_of ctxt));
+ val path = dir + Path.explode name handle ERROR msg => err msg;
+ val path = Path.expand path handle ERROR msg => err msg;
+ val path' = Path.implode path;
+ val _ = Context_Position.report ctxt pos (Markup.path path');
+ val _ : Path.T = check_file path handle ERROR msg => err msg;
+ in path' end;
+
+ val check_file = formal_check File.check_file;
+ val check_dir = formal_check File.check_dir;
end
\<close>
@@ -244,7 +249,7 @@ type ('transitionM, 'Proof_stateM, 'state) toplevel =
, keep: ('state -> unit) -> 'transitionM
, generic_theory: (generic_theory -> generic_theory) -> 'transitionM
, theory: (theory -> theory) -> 'transitionM
- , begin_local_theory: bool -> (theory -> local_theory) -> 'transitionM
+ , begin_main_target: bool -> (theory -> local_theory) -> 'transitionM
, local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
(bool -> local_theory -> local_theory) -> 'transitionM
, local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
@@ -446,7 +451,7 @@ fun semi__command_proof top = let open META_overload
end
fun end' top =
- (\<^command_keyword>\<open>end\<close>, #tr_raw top (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
+ (\<^command_keyword>\<open>end\<close>, #tr_raw top (Toplevel.exit o Toplevel.end_main_target o Toplevel.end_nested_target o
Toplevel.end_proof (K Proof.end_notepad)))
structure Cmd = struct open META open META_overload
@@ -608,13 +613,13 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
| Theory_type_notation type_notation =>
cons (\<^command_keyword>\<open>type_notation\<close>, Cmd.type_notation top type_notation)
| Theory_instantiation (Instantiation (n, n_def, expr)) => let val name = To_string0 n in fn acc => acc
- |>:: (\<^command_keyword>\<open>instantiation\<close>, #begin_local_theory top true (Cmd.instantiation1 name))
+ |>:: (\<^command_keyword>\<open>instantiation\<close>, #begin_main_target top true (Cmd.instantiation1 name))
|>:: (\<^command_keyword>\<open>definition\<close>, #local_theory' top NONE NONE (#2 oo Cmd.instantiation2 name n_def expr))
|>:: (\<^command_keyword>\<open>instance\<close>, #local_theory_to_proof top NONE NONE (Class.instantiation_instance I))
|>:: (\<^command_keyword>\<open>..\<close>, #tr_raw top Isar_Cmd.default_proof)
|>:: end' top end
| Theory_overloading (Overloading (n_c, e_c, n, e)) => (fn acc => acc
- |>:: (\<^command_keyword>\<open>overloading\<close>, #begin_local_theory top true (Cmd.overloading1 n_c e_c))
+ |>:: (\<^command_keyword>\<open>overloading\<close>, #begin_main_target top true (Cmd.overloading1 n_c e_c))
|>:: (\<^command_keyword>\<open>definition\<close>, #local_theory' top NONE NONE (Cmd.overloading2 n e))
|>:: end' top)
| Theory_consts consts =>
@@ -785,6 +790,7 @@ local
|> ( Expression.add_locale_cmd
(To_sbinding (META.holThyLocale_name data))
Binding.empty
+ []
([], [])
(List.concat
(map
@@ -831,7 +837,7 @@ fun all_meta_tr aux top thy_o = fn
(case theo of
Theories_one theo => Command_Transition.semi__theory top theo
| Theories_locale (data, l) => fn acc => acc
- |>:: (\<^command_keyword>\<open>locale\<close>, #begin_local_theory top true (semi__locale data))
+ |>:: (\<^command_keyword>\<open>locale\<close>, #begin_main_target top true (semi__locale data))
|> fold (fold (Command_Transition.semi__theory top)) l
|>:: end' top)
| META_boot_generation_syntax _ => I
@@ -860,7 +866,7 @@ fun all_meta_thy aux top_theory top_local_theory = fn
META_semi_theories theo => apsnd
(case theo of
Theories_one theo => Command_Theory.semi__theory top_theory theo
- | Theories_locale (data, l) => (*Toplevel.begin_local_theory*) fn thy => thy
+ | Theories_locale (data, l) => (*Toplevel.begin_main_target*) fn thy => thy
|> semi__locale data
|> fold (fold (Command_Theory.semi__theory top_local_theory)) l
|> Local_Theory.exit_global)
@@ -1200,12 +1206,12 @@ fun thy_shallow l_obj get_all_meta_embed =
(fn msg =>
let val () = disp_time msg ()
fun in_self f =
- \<comment> \<open>Note: This function is not equivalent to \<^ML>\<open>Local_Theory.subtarget\<close>.\<close>
+ \<comment> \<open>Note: This function is not equivalent to \<^ML>\<open>Local_Theory.begin_nested\<close> \<^ML>\<open>Local_Theory.end_nested\<close>.\<close>
Local_Theory.new_group
#> f
#> Local_Theory.reset_group
#> (fn lthy =>
- #1 (Named_Target.switch NONE (Context.Proof lthy)) lthy |> Context.the_proof)
+ #1 (Target_Context.switch_named_cmd NONE (Context.Proof lthy)) lthy |> Context.the_proof)
fun not_used p _ = error ("not used " ^ Position.here p)
val context_of = I
fun proof' f = f true
@@ -1226,7 +1232,7 @@ fun thy_shallow l_obj get_all_meta_embed =
, tr_report = report, tr_report_o = report_o
, pr_report = report, pr_report_o = report_o
(* irrelevant part *)
- , begin_local_theory = K o not_used \<^here>
+ , begin_main_target = K o not_used \<^here>
, local_theory_to_proof' = K o K not_used \<^here>
, local_theory_to_proof = K o K not_used \<^here>
, tr_raw = not_used \<^here> }
@@ -1243,7 +1249,7 @@ fun thy_shallow l_obj get_all_meta_embed =
, tr_report = report, tr_report_o = report_o
, pr_report = report, pr_report_o = report_o
(* irrelevant part *)
- , begin_local_theory = K o not_used \<^here>
+ , begin_main_target = K o not_used \<^here>
, local_theory_to_proof' = K o K not_used \<^here>
, local_theory_to_proof = K o K not_used \<^here>
, tr_raw = not_used \<^here> }
@@ -1331,7 +1337,7 @@ fun outer_syntax_commands'''' is_safe mk_string get_all_meta_embed name thy _ =
, keep = Toplevel.keep
, generic_theory = Toplevel.generic_theory
, theory = Toplevel.theory
- , begin_local_theory = Toplevel.begin_local_theory
+ , begin_main_target = Toplevel.begin_main_target
, local_theory' = Toplevel.local_theory'
, local_theory = Toplevel.local_theory
, local_theory_to_proof' = Toplevel.local_theory_to_proof'
@@ -1693,7 +1699,7 @@ structure USE_parse = struct
-- optional_b \<^keyword>\<open>ignore_not_in_scope\<close>
-- optional_b \<^keyword>\<open>abstract_mutual_data_params\<close>
-- optional_b \<^keyword>\<open>concat_modules\<close>
- -- Scan.option (\<^keyword>\<open>base_path\<close> |-- Parse.position Parse.path)
+ -- Scan.option (\<^keyword>\<open>base_path\<close> |-- Parse.path_input)
-- Scan.optional (parse_l' (Parse.name -- Scan.option ((\<^keyword>\<open>\<rightharpoonup>\<close> || \<^keyword>\<open>=>\<close>) |-- Parse.name))) []
end
\<close>
@@ -1929,7 +1935,7 @@ local
val haskabelle_bin = haskabelle_path "HASKABELLE_HOME" ["bin", "haskabelle_bin"]
val haskabelle_default = haskabelle_path "HASKABELLE_HOME_USER" ["default"]
in
- fun parse meta_parse_shallow meta_parse_imports meta_parse_code meta_parse_functions hsk_name check_dir hsk_str ((((((((old_datatype, try_import), only_types), ignore_not_in_scope), abstract_mutual_data_params), concat_modules), base_path_abs), l_rewrite), (content, pos)) thy =
+ fun parse meta_parse_shallow meta_parse_imports meta_parse_code meta_parse_functions hsk_name check_dir hsk_str ((((((((old_datatype, try_import), only_types), ignore_not_in_scope), abstract_mutual_data_params), concat_modules), base_path_abs), l_rewrite), source) thy =
let fun string_of_bool b = if b then "true" else "false"
val st =
Bash.process
@@ -1939,7 +1945,7 @@ in
, "--export", "false"
, "--try-import", string_of_bool try_import
, "--only-types", string_of_bool only_types
- , "--base-path-abs", case base_path_abs of NONE => "" | SOME s => check_dir thy s
+ , "--base-path-abs", case base_path_abs of NONE => "" | SOME source => check_dir (Proof_Context.init_global thy) NONE source
, "--ignore-not-in-scope", string_of_bool ignore_not_in_scope
, "--abstract-mutual-data-params", string_of_bool abstract_mutual_data_params
, "--dump-output"
@@ -1950,9 +1956,9 @@ in
[ "--hsk-name" ] @ the_list hsk_name
@ (case
if hsk_str then
- ([ Bash.string content ], [])
+ ([ Bash.string (Input.string_of source) ], [])
else
- ([], [ Resources'.check_path' (SOME File.check_file) (Proof_Context.init_global thy) Path.current (content, pos) ])
+ ([], [ Resources'.check_file (Proof_Context.init_global thy) (SOME Path.current) source ])
of (cts, files) => List.concat [ ["--hsk-contents"], cts, ["--files"], files ])))
in
if #rc st = 0 then
@@ -1979,7 +1985,7 @@ in
:: acc)
end)
l_rep
- (Symbol.explode content, (Position.advance_offsets 1 pos, 0), [])
+ (Symbol.explode (Input.string_of source), (Position.advance_offsets 1 (Input.pos_of source), 0), [])
|> #3
in Position.reports l_rep end)
l_rep
@@ -2001,7 +2007,7 @@ end
local
type haskell_parse =
- (((((((bool * Code_Numeral.natural) * bool) * bool) * bool) * bool) * bool) * (string * Position.T) option)
+ (((((((bool * Code_Numeral.natural) * bool) * bool) * bool) * bool) * bool) * Input.source option)
* (string * string option) list
structure Data_lang = Theory_Data
@@ -2010,16 +2016,20 @@ local
val extend = I
val merge = Name_Space.merge_tables)
+ structure Parse' =
+ struct
+ val haskell_source = Parse.input (Parse.group (fn () => "Haskell source") Parse.text)
+ end
open USE_parse
in
val () =
outer_syntax_commands'2 \<^mk_string> \<^command_keyword>\<open>Haskell\<close> ""
- (haskell_parse -- Parse.position Parse.cartouche)
+ (haskell_parse -- Parse'.haskell_source)
(get_thy \<^here> o parse' true)
val () =
outer_syntax_commands'2 \<^mk_string> \<^command_keyword>\<open>Haskell_file\<close> ""
- (haskell_parse -- Parse.position Parse.path)
+ (haskell_parse -- Parse.path_input)
(get_thy \<^here> o parse' false)
val () =
@@ -2052,14 +2062,14 @@ val () =
(#2 o Name_Space.define
(Context.Theory thy)
true
- (lang, (hsk_arg, Option.map (Resources'.check_dir thy) base_path, imports, defines, functions)))
+ (lang, (hsk_arg, Option.map (Resources'.check_dir (Proof_Context.init_global thy) NONE) base_path, imports, defines, functions)))
thy)
end))
val () =
outer_syntax_commands'2 \<^mk_string> \<^command_keyword>\<open>language\<close> ""
(Scan.optional (\<^keyword>\<open>meta\<close> >> K true) false
- -- Parse.binding --| Parse.$$$ "::" -- Parse.position Parse.name --| Parse.where_ -- Parse.position Parse.cartouche)
+ -- Parse.binding --| Parse.$$$ "::" -- Parse.position Parse.name --| Parse.where_ -- Parse'.haskell_source)
(fn (((is_shallow, prog), lang), code) =>
get_thy \<^here>
(fn thy =>
@@ -2071,7 +2081,7 @@ val () =
(SOME defines)
(functions (From.string prog'))
(SOME prog')
- (K (K (case hsk_path of NONE => "" | SOME s => s)))
+ (K (K (K (case hsk_path of NONE => "" | SOME s => s))))
true
(hsk_arg, code)
thy
diff --git a/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy b/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
index 2063ab351df..4b48c444b7a 100644
--- a/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
+++ b/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
@@ -195,23 +195,28 @@ structure Toplevel' = struct
end
structure Resources' = struct
- fun check_path' check_file ctxt dir (name, pos) =
+ fun formal_check check_file ctxt opt_dir source =
let
- fun err msg pos = error (msg ^ Position.here pos)
- val _ = Context_Position.report ctxt pos Markup.language_path;
+ val name = Input.string_of source;
+ val pos = Input.pos_of source;
+ val delimited = Input.is_delimited source;
- val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
- val path' = Path.expand path handle ERROR msg => err msg pos;
- val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
- val _ =
- (case check_file of
- NONE => path
- | SOME check => (check path handle ERROR msg => err msg pos));
- in Path.implode path' end
-
- fun check_dir thy = check_path' (SOME File.check_dir)
- (Proof_Context.init_global thy)
- (Resources.master_directory thy)
+ val _ = Context_Position.report ctxt pos (Markup.language_path delimited);
+
+ fun err msg = error (msg ^ Position.here pos);
+ val dir =
+ (case opt_dir of
+ SOME dir => dir
+ | NONE => Resources.master_directory (Proof_Context.theory_of ctxt));
+ val path = dir + Path.explode name handle ERROR msg => err msg;
+ val path' = Path.implode_symbolic path;
+ val _ = Path.expand path handle ERROR msg => err msg;
+ val _ = Context_Position.report ctxt pos (Markup.path path');
+ val _ : Path.T = check_file path handle ERROR msg => err msg;
+ in path' end;
+
+ val check_file = formal_check File.check_file;
+ val check_dir = formal_check File.check_dir;
end
\<close>
@@ -252,7 +257,7 @@ type ('transitionM, 'Proof_stateM, 'state) toplevel =
, keep: ('state -> unit) -> 'transitionM
, generic_theory: (generic_theory -> generic_theory) -> 'transitionM
, theory: (theory -> theory) -> 'transitionM
- , begin_local_theory: bool -> (theory -> local_theory) -> 'transitionM
+ , begin_main_target: bool -> (theory -> local_theory) -> 'transitionM
, local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
(bool -> local_theory -> local_theory) -> 'transitionM
, local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
@@ -454,7 +459,7 @@ fun semi__command_proof top = let open META_overload
end
fun end' top =
- (\<^command_keyword>\<open>end\<close>, #tr_raw top (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
+ (\<^command_keyword>\<open>end\<close>, #tr_raw top (Toplevel.exit o Toplevel.end_main_target o Toplevel.end_nested_target o
Toplevel.end_proof (K Proof.end_notepad)))
structure Cmd = struct open META open META_overload
@@ -616,13 +621,13 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
| Theory_type_notation type_notation =>
cons (\<^command_keyword>\<open>type_notation\<close>, Cmd.type_notation top type_notation)
| Theory_instantiation (Instantiation (n, n_def, expr)) => let val name = To_string0 n in fn acc => acc
- |>:: (\<^command_keyword>\<open>instantiation\<close>, #begin_local_theory top true (Cmd.instantiation1 name))
+ |>:: (\<^command_keyword>\<open>instantiation\<close>, #begin_main_target top true (Cmd.instantiation1 name))
|>:: (\<^command_keyword>\<open>definition\<close>, #local_theory' top NONE NONE (#2 oo Cmd.instantiation2 name n_def expr))
|>:: (\<^command_keyword>\<open>instance\<close>, #local_theory_to_proof top NONE NONE (Class.instantiation_instance I))
|>:: (\<^command_keyword>\<open>..\<close>, #tr_raw top Isar_Cmd.default_proof)
|>:: end' top end
| Theory_overloading (Overloading (n_c, e_c, n, e)) => (fn acc => acc
- |>:: (\<^command_keyword>\<open>overloading\<close>, #begin_local_theory top true (Cmd.overloading1 n_c e_c))
+ |>:: (\<^command_keyword>\<open>overloading\<close>, #begin_main_target top true (Cmd.overloading1 n_c e_c))
|>:: (\<^command_keyword>\<open>definition\<close>, #local_theory' top NONE NONE (Cmd.overloading2 n e))
|>:: end' top)
| Theory_consts consts =>
@@ -793,6 +798,7 @@ local
|> ( Expression.add_locale_cmd
(To_sbinding (META.holThyLocale_name data))
Binding.empty
+ []
([], [])
(List.concat
(map
@@ -839,7 +845,7 @@ fun all_meta_tr aux top thy_o = fn
(case theo of
Theories_one theo => Command_Transition.semi__theory top theo
| Theories_locale (data, l) => fn acc => acc
- |>:: (\<^command_keyword>\<open>locale\<close>, #begin_local_theory top true (semi__locale data))
+ |>:: (\<^command_keyword>\<open>locale\<close>, #begin_main_target top true (semi__locale data))
|> fold (fold (Command_Transition.semi__theory top)) l
|>:: end' top)
| META_boot_generation_syntax _ => I
@@ -868,7 +874,7 @@ fun all_meta_thy aux top_theory top_local_theory = fn
META_semi_theories theo => apsnd
(case theo of
Theories_one theo => Command_Theory.semi__theory top_theory theo
- | Theories_locale (data, l) => (*Toplevel.begin_local_theory*) fn thy => thy
+ | Theories_locale (data, l) => (*Toplevel.begin_main_target*) fn thy => thy
|> semi__locale data
|> fold (fold (Command_Theory.semi__theory top_local_theory)) l
|> Local_Theory.exit_global)
@@ -1363,7 +1369,7 @@ fun f_command l_mode =
let val tmp_export_code = Deep.mk_path_export_code (#tmp_export_code i_deep) ml_compiler i
fun mk_fic s = Path.append tmp_export_code (Path.make [s])
val () = Deep0.Find.check_compil ml_compiler ()
- val () = Isabelle_System.mkdirs tmp_export_code in
+ val () = Isabelle_System.mkdir(*TODO?*) tmp_export_code in
(( ( (ml_compiler, ml_module)
, ( Path.implode (if Deep0.Find.export_mode ml_compiler = Deep0.Export_code_env.Directory then
tmp_export_code
@@ -1571,12 +1577,12 @@ fun thy_shallow l_obj get_all_meta_embed =
(fn msg =>
let val () = disp_time msg ()
fun in_self f =
- \<comment> \<open>Note: This function is not equivalent to \<^ML>\<open>Local_Theory.subtarget\<close>.\<close>
+ \<comment> \<open>Note: This function is not equivalent to \<^ML>\<open>Local_Theory.begin_nested\<close> \<^ML>\<open>Local_Theory.end_nested\<close>.\<close>
Local_Theory.new_group
#> f
#> Local_Theory.reset_group
#> (fn lthy =>
- #1 (Named_Target.switch NONE (Context.Proof lthy)) lthy |> Context.the_proof)
+ #1 (Target_Context.switch_named_cmd NONE (Context.Proof lthy)) lthy |> Context.the_proof)
fun not_used p _ = error ("not used " ^ Position.here p)
val context_of = I
fun proof' f = f true
@@ -1597,7 +1603,7 @@ fun thy_shallow l_obj get_all_meta_embed =
, tr_report = report, tr_report_o = report_o
, pr_report = report, pr_report_o = report_o
(* irrelevant part *)
- , begin_local_theory = K o not_used \<^here>
+ , begin_main_target = K o not_used \<^here>
, local_theory_to_proof' = K o K not_used \<^here>
, local_theory_to_proof = K o K not_used \<^here>
, tr_raw = not_used \<^here> }
@@ -1614,7 +1620,7 @@ fun thy_shallow l_obj get_all_meta_embed =
, tr_report = report, tr_report_o = report_o
, pr_report = report, pr_report_o = report_o
(* irrelevant part *)
- , begin_local_theory = K o not_used \<^here>
+ , begin_main_target = K o not_used \<^here>
, local_theory_to_proof' = K o K not_used \<^here>
, local_theory_to_proof = K o K not_used \<^here>
, tr_raw = not_used \<^here> }
@@ -1702,7 +1708,7 @@ fun outer_syntax_commands'''' is_safe mk_string get_all_meta_embed name thy _ =
, keep = Toplevel.keep
, generic_theory = Toplevel.generic_theory
, theory = Toplevel.theory
- , begin_local_theory = Toplevel.begin_local_theory
+ , begin_main_target = Toplevel.begin_main_target
, local_theory' = Toplevel.local_theory'
, local_theory = Toplevel.local_theory
, local_theory_to_proof' = Toplevel.local_theory_to_proof'
diff --git a/Citadelle/src/compiler_citadelle_c/ex/C_Model_ex_hol.thy b/Citadelle/src/compiler_citadelle_c/ex/C_Model_ex_hol.thy
index 15d3b0fd5d9..1341f07405b 100644
--- a/Citadelle/src/compiler_citadelle_c/ex/C_Model_ex_hol.thy
+++ b/Citadelle/src/compiler_citadelle_c/ex/C_Model_ex_hol.thy
@@ -92,7 +92,7 @@ ML\<open>open META2\<close>
section \<open>Initialization of the parsing code\<close>
meta_language C
- base_path "../src/compiler_generic/isabelle_home/contrib/haskabelle"
+ base_path "../../../src/compiler_generic/isabelle_home/contrib/haskabelle"
[Prelude \<rightharpoonup> C_Model_init, Option \<rightharpoonup> C_Model_init]
where imports \<open>Language.C\<close>
(load \<open>Importer.Conversion.Haskell\<close>)
@@ -101,6 +101,19 @@ meta_language C
section \<open>Parsing\<close>
+definition increment_method :: unit where \<open>
+ increment_method = ()
+\<close>
+
+definition even_count_gen :: unit where \<open>
+ even_count_gen = ()
+\<close>
+
+definition max_program_correct :: unit where \<open>
+ max_program_correct = ()
+\<close>
+
+(*
language increment_method :: C where \<open>/* ASSUMES \<open>\<guillemotleft>a\<guillemotright> >\<^sub>u 0\<close> */ f () {
int x = 0;
/* INVAR \<open>\<guillemotleft>a\<guillemotright> >\<^sub>u 0 \<and> \<guillemotleft>a\<guillemotright> \<ge>\<^sub>u &x\<close>
@@ -133,5 +146,6 @@ language max_program_correct :: C where \<open>/* ASSUMES \<open>uop length \<gu
i = i + 1;
}
} /* ENSURES \<open>&r =\<^sub>u uop Max (uop set \<guillemotleft>a\<guillemotright>)\<close> */\<close>
+*)
end
diff --git a/Citadelle/src/compiler_citadelle_c/ex/C_Model_ex_meta.thy b/Citadelle/src/compiler_citadelle_c/ex/C_Model_ex_meta.thy
index 21be53ad31a..fff12942104 100644
--- a/Citadelle/src/compiler_citadelle_c/ex/C_Model_ex_meta.thy
+++ b/Citadelle/src/compiler_citadelle_c/ex/C_Model_ex_meta.thy
@@ -92,7 +92,7 @@ ML\<open>open META2\<close>
section \<open>Initialization of the parsing code\<close>
meta_language C
- base_path "../src/compiler_generic/isabelle_home/contrib/haskabelle"
+ base_path "../../../src/compiler_generic/isabelle_home/contrib/haskabelle"
[Prelude, Option]
where imports \<open>Language.C\<close>
(load \<open>Importer.Conversion.Haskell\<close>)
@@ -101,6 +101,19 @@ meta_language C
section \<open>Parsing\<close>
+definition increment_method :: unit where \<open>
+ increment_method = ()
+\<close>
+
+definition even_count_gen :: unit where \<open>
+ even_count_gen = ()
+\<close>
+
+definition max_program_correct :: unit where \<open>
+ max_program_correct = ()
+\<close>
+
+(*
language meta increment_method :: C where \<open>/* ASSUMES \<open>\<guillemotleft>a\<guillemotright> >\<^sub>u 0\<close> */ f () {
int x = 0;
/* INVAR \<open>\<guillemotleft>a\<guillemotright> >\<^sub>u 0 \<and> \<guillemotleft>a\<guillemotright> \<ge>\<^sub>u &x\<close>
@@ -133,5 +146,5 @@ language meta max_program_correct :: C where \<open>/* ASSUMES \<open>uop length
i = i + 1;
}
} /* ENSURES \<open>&r =\<^sub>u uop Max (uop set \<guillemotleft>a\<guillemotright>)\<close> */\<close>
-
+*)
end
diff --git a/Citadelle/src/compiler_generic/toy_example/embedding/Generator_dynamic_sequential.thy b/Citadelle/src/compiler_generic/toy_example/embedding/Generator_dynamic_sequential.thy
index 8efb23a6663..6b36a5b78e7 100644
--- a/Citadelle/src/compiler_generic/toy_example/embedding/Generator_dynamic_sequential.thy
+++ b/Citadelle/src/compiler_generic/toy_example/embedding/Generator_dynamic_sequential.thy
@@ -241,7 +241,7 @@ type ('transitionM, 'Proof_stateM, 'state) toplevel =
, keep: ('state -> unit) -> 'transitionM
, generic_theory: (generic_theory -> generic_theory) -> 'transitionM
, theory: (theory -> theory) -> 'transitionM
- , begin_local_theory: bool -> (theory -> local_theory) -> 'transitionM
+ , begin_main_target: bool -> (theory -> local_theory) -> 'transitionM
, local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
(bool -> local_theory -> local_theory) -> 'transitionM
, local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
@@ -443,7 +443,7 @@ fun semi__command_proof top = let open META_overload
end
fun end' top =
- (\<^command_keyword>\<open>end\<close>, #tr_raw top (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
+ (\<^command_keyword>\<open>end\<close>, #tr_raw top (Toplevel.exit o Toplevel.end_main_target o Toplevel.end_nested_target o
Toplevel.end_proof (K Proof.end_notepad)))
structure Cmd = struct open META open META_overload
@@ -605,13 +605,13 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
| Theory_type_notation type_notation =>
cons (\<^command_keyword>\<open>type_notation\<close>, Cmd.type_notation top type_notation)
| Theory_instantiation (Instantiation (n, n_def, expr)) => let val name = To_string0 n in fn acc => acc
- |>:: (\<^command_keyword>\<open>instantiation\<close>, #begin_local_theory top true (Cmd.instantiation1 name))
+ |>:: (\<^command_keyword>\<open>instantiation\<close>, #begin_main_target top true (Cmd.instantiation1 name))
|>:: (\<^command_keyword>\<open>definition\<close>, #local_theory' top NONE NONE (#2 oo Cmd.instantiation2 name n_def expr))
|>:: (\<^command_keyword>\<open>instance\<close>, #local_theory_to_proof top NONE NONE (Class.instantiation_instance I))
|>:: (\<^command_keyword>\<open>..\<close>, #tr_raw top Isar_Cmd.default_proof)
|>:: end' top end
| Theory_overloading (Overloading (n_c, e_c, n, e)) => (fn acc => acc
- |>:: (\<^command_keyword>\<open>overloading\<close>, #begin_local_theory top true (Cmd.overloading1 n_c e_c))
+ |>:: (\<^command_keyword>\<open>overloading\<close>, #begin_main_target top true (Cmd.overloading1 n_c e_c))
|>:: (\<^command_keyword>\<open>definition\<close>, #local_theory' top NONE NONE (Cmd.overloading2 n e))
|>:: end' top)
| Theory_consts consts =>
@@ -782,6 +782,7 @@ local
|> ( Expression.add_locale_cmd
(To_sbinding (META.holThyLocale_name data))
Binding.empty
+ []
([], [])
(List.concat
(map
@@ -828,7 +829,7 @@ fun all_meta_tr aux top thy_o = fn
(case theo of
Theories_one theo => Command_Transition.semi__theory top theo
| Theories_locale (data, l) => fn acc => acc
- |>:: (\<^command_keyword>\<open>locale\<close>, #begin_local_theory top true (semi__locale data))
+ |>:: (\<^command_keyword>\<open>locale\<close>, #begin_main_target top true (semi__locale data))
|> fold (fold (Command_Transition.semi__theory top)) l
|>:: end' top)
| META_boot_generation_syntax _ => I
@@ -857,7 +858,7 @@ fun all_meta_thy aux top_theory top_local_theory = fn
META_semi_theories theo => apsnd
(case theo of
Theories_one theo => Command_Theory.semi__theory top_theory theo
- | Theories_locale (data, l) => (*Toplevel.begin_local_theory*) fn thy => thy
+ | Theories_locale (data, l) => (*Toplevel.begin_main_target*) fn thy => thy
|> semi__locale data
|> fold (fold (Command_Theory.semi__theory top_local_theory)) l
|> Local_Theory.exit_global)
@@ -1197,12 +1198,12 @@ fun thy_shallow l_obj get_all_meta_embed =
(fn msg =>
let val () = disp_time msg ()
fun in_self f =
- \<comment> \<open>Note: This function is not equivalent to \<^ML>\<open>Local_Theory.subtarget\<close>.\<close>
+ \<comment> \<open>Note: This function is not equivalent to \<^ML>\<open>Local_Theory.begin_nested\<close> \<^ML>\<open>Local_Theory.end_nested\<close>.\<close>
Local_Theory.new_group
#> f
#> Local_Theory.reset_group
#> (fn lthy =>
- #1 (Named_Target.switch NONE (Context.Proof lthy)) lthy |> Context.the_proof)
+ #1 (Target_Context.switch_named_cmd NONE (Context.Proof lthy)) lthy |> Context.the_proof)
fun not_used p _ = error ("not used " ^ Position.here p)
val context_of = I
fun proof' f = f true
@@ -1223,7 +1224,7 @@ fun thy_shallow l_obj get_all_meta_embed =
, tr_report = report, tr_report_o = report_o
, pr_report = report, pr_report_o = report_o
(* irrelevant part *)
- , begin_local_theory = K o not_used \<^here>
+ , begin_main_target = K o not_used \<^here>
, local_theory_to_proof' = K o K not_used \<^here>
, local_theory_to_proof = K o K not_used \<^here>
, tr_raw = not_used \<^here> }
@@ -1240,7 +1241,7 @@ fun thy_shallow l_obj get_all_meta_embed =
, tr_report = report, tr_report_o = report_o
, pr_report = report, pr_report_o = report_o
(* irrelevant part *)
- , begin_local_theory = K o not_used \<^here>
+ , begin_main_target = K o not_used \<^here>
, local_theory_to_proof' = K o K not_used \<^here>
, local_theory_to_proof = K o K not_used \<^here>
, tr_raw = not_used \<^here> }
@@ -1328,7 +1329,7 @@ fun outer_syntax_commands'''' is_safe mk_string get_all_meta_embed name thy _ =
, keep = Toplevel.keep
, generic_theory = Toplevel.generic_theory
, theory = Toplevel.theory
- , begin_local_theory = Toplevel.begin_local_theory
+ , begin_main_target = Toplevel.begin_main_target
, local_theory' = Toplevel.local_theory'
, local_theory = Toplevel.local_theory
, local_theory_to_proof' = Toplevel.local_theory_to_proof'
diff --git a/Citadelle/src/compiler_misc/meta/Printer_init.thy b/Citadelle/src/compiler_misc/meta/Printer_init.thy
index f99c23417d4..a3286a211da 100644
--- a/Citadelle/src/compiler_misc/meta/Printer_init.thy
+++ b/Citadelle/src/compiler_misc/meta/Printer_init.thy
@@ -111,23 +111,29 @@ val parse_inst_ident = Parse.name --| \<^keyword>\<open>::\<close> -- Parse.clas
(* 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.smart_implode 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_cmd all_public raw_cs seris lthy =
--
GitLab