equal
deleted
inserted
replaced
26 *** ML *** |
26 *** ML *** |
27 |
27 |
28 * Original PolyML.pointerEq is retained as a convenience for tools that |
28 * Original PolyML.pointerEq is retained as a convenience for tools that |
29 don't use Isabelle/ML (where this is called "pointer_eq"). |
29 don't use Isabelle/ML (where this is called "pointer_eq"). |
30 |
30 |
|
31 * ML evaluation (notably via commands 'ML' and 'ML_file') is subject to |
|
32 option ML_environment to select a named environment, such as "Isabelle" |
|
33 for Isabelle/ML, or "SML" for official Standard ML. It is also possible |
|
34 to move toplevel bindings between environments, using a notation with |
|
35 ">" as separator. For example: |
|
36 |
|
37 declare [[ML_environment = "Isabelle>SML"]] |
|
38 ML \<open>val println = writeln\<close> |
|
39 |
|
40 declare [[ML_environment = "SML"]] |
|
41 ML \<open>println "test"\<close> |
|
42 |
|
43 declare [[ML_environment = "Isabelle"]] |
|
44 ML \<open>println\<close> \<comment> \<open>not present\<close> |
|
45 |
|
46 The Isabelle/ML function ML_Env.setup defines new ML environments. This |
|
47 is useful to incorporate big SML projects in an isolated name space, and |
|
48 potentially with variations on ML syntax (existing ML_Env.SML_operations |
|
49 observes the official standard). |
31 |
50 |
32 |
51 |
33 New in Isabelle2018 (August 2018) |
52 New in Isabelle2018 (August 2018) |
34 --------------------------------- |
53 --------------------------------- |
35 |
54 |