From 2a06b7d82bb25edb3a5dc9830af89e3e94ecbb6d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?=
<tuong@users.noreply.github.com>
Date: Sun, 2 Jan 2022 17:07:28 -0800
Subject: [PATCH] simplify
---
C11-FrontEnd/examples/C2.thy | 4 ++--
C11-FrontEnd/examples/C_paper.thy | 7 ++-----
C11-FrontEnd/src/C_Command.thy | 32 ++++++++++++++++++-------------
3 files changed, 23 insertions(+), 20 deletions(-)
diff --git a/C11-FrontEnd/examples/C2.thy b/C11-FrontEnd/examples/C2.thy
index 89fa675e3d4..301fddf336d 100644
--- a/C11-FrontEnd/examples/C2.thy
+++ b/C11-FrontEnd/examples/C2.thy
@@ -376,8 +376,8 @@ subsection \<open>Continuation Calculus with the C Environment: Presentation in
declare [[C_parser_trace = false]]
ML\<open>
-fun C src = C_Module.C' (C_Module.env (Context.the_generic_context ())) src
-val C' = C_Module.C'
+val C = C_Module.C' NONE
+val C' = C_Module.C' o SOME
\<close>
C \<comment> \<open>Nesting C code without propagating the C environment\<close> \<open>
diff --git a/C11-FrontEnd/examples/C_paper.thy b/C11-FrontEnd/examples/C_paper.thy
index 4b8948be929..3ef693c4e03 100644
--- a/C11-FrontEnd/examples/C_paper.thy
+++ b/C11-FrontEnd/examples/C_paper.thy
@@ -50,17 +50,14 @@ ML\<open>
val _ = Theory.setup
(C_Inner_Syntax.command C_Inner_Isar_Cmd.setup' C_Parse.ML_source ("\<simeq>setup", \<^here>, \<^here>))
-val C' = C_Module.C'
-
-fun C opt = case opt of NONE => C' (C_Module.env (Context.the_generic_context ()))
- | SOME env => C' env
+val C = C_Module.C'
fun C_def dir name _ _ =
Context.map_theory
(C_Inner_Syntax.command'
(C_Inner_Syntax.drop1
(C_Scan.Right ( (fn src => fn context =>
- C' (C_Stack.Data_Lang.get' context |> #2) src context)
+ C_Module.C' (SOME (C_Stack.Data_Lang.get' context |> #2)) src context)
, dir)))
C_Parse.C_source
name)
diff --git a/C11-FrontEnd/src/C_Command.thy b/C11-FrontEnd/src/C_Command.thy
index 9b830b5d4a3..3a09dad7f94 100644
--- a/C11-FrontEnd/src/C_Command.thy
+++ b/C11-FrontEnd/src/C_Command.thy
@@ -360,19 +360,25 @@ fun C source =
exec_eval source
#> Local_Theory.propagate_ml_env
-fun C' env_lang src context =
- context
- |> C_Env.empty_env_tree
- |> C_Context.eval_source'
- env_lang
- (fn src => start src context)
- err
- accept
- src
- |> (fn (_, {context, reports_text, error_lines}) =>
- tap (fn _ => case error_lines of [] => () | l => warning (cat_lines (rev l)))
- (C_Stack.Data_Tree.map (curry C_Stack.Data_Tree_Args.merge (reports_text, []))
- context))
+val C' =
+ let
+ fun C env_lang src context =
+ context
+ |> C_Env.empty_env_tree
+ |> C_Context.eval_source'
+ env_lang
+ (fn src => start src context)
+ err
+ accept
+ src
+ |> (fn (_, {context, reports_text, error_lines}) =>
+ tap (fn _ => case error_lines of [] => () | l => warning (cat_lines (rev l)))
+ (C_Stack.Data_Tree.map (curry C_Stack.Data_Tree_Args.merge (reports_text, []))
+ context))
+ in
+ fn NONE => (fn src => C (env (Context.the_generic_context ())) src)
+ | SOME env_lang => C env_lang
+ end
fun C_export_file (pos, _) lthy =
let
--
GitLab