equal
deleted
inserted
replaced
84 |
84 |
85 The Isabelle/ML function ML_Env.setup defines new ML environments. This |
85 The Isabelle/ML function ML_Env.setup defines new ML environments. This |
86 is useful to incorporate big SML projects in an isolated name space, and |
86 is useful to incorporate big SML projects in an isolated name space, and |
87 potentially with variations on ML syntax (existing ML_Env.SML_operations |
87 potentially with variations on ML syntax (existing ML_Env.SML_operations |
88 observes the official standard). |
88 observes the official standard). |
|
89 |
|
90 * GHC.read_source reads Haskell source text with antiquotations (only |
|
91 the control-cartouche form). The default "cartouche" antiquotation |
|
92 evaluates an ML expression of type string and inlines the result as |
|
93 Haskell string literal. This allows to refer to Isabelle items robustly, |
|
94 e.g. via Isabelle/ML antiquotations or library operations. For example: |
|
95 |
|
96 ML \<open> |
|
97 GHC.read_source \<^context> \<open> |
|
98 allConst, impConst, eqConst :: String |
|
99 allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close> |
|
100 impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close> |
|
101 eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close> |
|
102 \<close> |
|
103 |> File.write \<^path>\<open>consts.hs\<close> |
|
104 \<close> |
89 |
105 |
90 |
106 |
91 *** System *** |
107 *** System *** |
92 |
108 |
93 * Isabelle server command "use_theories" supports "nodes_status_delay" |
109 * Isabelle server command "use_theories" supports "nodes_status_delay" |