author | wenzelm |
Tue, 26 May 2020 12:09:36 +0200 | |
changeset 71897 | 2cf0b0293f0d |
parent 71892 | dff81ce866d4 |
child 71907 | 64c9628b39fc |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
61575 | 2 |
|
47825 | 3 |
theory Scala |
4 |
imports Base |
|
5 |
begin |
|
6 |
||
58618 | 7 |
chapter \<open>Isabelle/Scala development tools\<close> |
47825 | 8 |
|
61575 | 9 |
text \<open> |
10 |
Isabelle/ML and Isabelle/Scala are the two main language environments for |
|
11 |
Isabelle tool implementations. There are some basic command-line tools to |
|
12 |
work with the underlying Java Virtual Machine, the Scala toplevel and |
|
13 |
compiler. Note that Isabelle/jEdit @{cite "isabelle-jedit"} provides a Scala |
|
14 |
Console for interactive experimentation within the running application. |
|
15 |
\<close> |
|
47825 | 16 |
|
17 |
||
58618 | 18 |
section \<open>Java Runtime Environment within Isabelle \label{sec:tool-java}\<close> |
47825 | 19 |
|
61575 | 20 |
text \<open> |
21 |
The @{tool_def java} tool is a direct wrapper for the Java Runtime |
|
22 |
Environment, within the regular Isabelle settings environment |
|
23 |
(\secref{sec:settings}). The command line arguments are that of the |
|
24 |
underlying Java version. It is run in \<^verbatim>\<open>-server\<close> mode if possible, to |
|
25 |
improve performance (at the cost of extra startup time). |
|
47825 | 26 |
|
61575 | 27 |
The \<^verbatim>\<open>java\<close> executable is the one within @{setting ISABELLE_JDK_HOME}, |
28 |
according to the standard directory layout for official JDK distributions. |
|
29 |
The class loader is augmented such that the name space of |
|
30 |
\<^verbatim>\<open>Isabelle/Pure.jar\<close> is available, which is the main Isabelle/Scala module. |
|
58618 | 31 |
\<close> |
47825 | 32 |
|
33 |
||
58618 | 34 |
section \<open>Scala toplevel \label{sec:tool-scala}\<close> |
47825 | 35 |
|
61575 | 36 |
text \<open> |
37 |
The @{tool_def scala} tool is a direct wrapper for the Scala toplevel; see |
|
38 |
also @{tool java} above. The command line arguments are that of the |
|
71897 | 39 |
underlying Scala version. This allows to interact with Isabelle/Scala in TTY |
40 |
mode. An alternative is to use the \<^verbatim>\<open>Console/Scala\<close> plugin of Isabelle/jEdit |
|
41 |
@{cite "isabelle-jedit"}. |
|
42 |
\<close> |
|
43 |
||
44 |
subsubsection \<open>Example\<close> |
|
47825 | 45 |
|
71897 | 46 |
text \<open> |
47 |
Explore the Isabelle system environment in Scala: |
|
48 |
@{scala [display] |
|
49 |
\<open>import isabelle._ |
|
50 |
||
51 |
val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME") |
|
52 |
||
53 |
val options = Options.init() |
|
54 |
options.bool("browser_info") |
|
55 |
options.string("document")\<close>} |
|
58618 | 56 |
\<close> |
47825 | 57 |
|
58 |
||
58618 | 59 |
section \<open>Scala compiler \label{sec:tool-scalac}\<close> |
47825 | 60 |
|
61575 | 61 |
text \<open> |
62 |
The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see |
|
63 |
also @{tool scala} above. The command line arguments are that of the |
|
64 |
underlying Scala version. |
|
47825 | 65 |
|
66 |
This allows to compile further Scala modules, depending on existing |
|
61575 | 67 |
Isabelle/Scala functionality. The resulting class or jar files can be added |
68 |
to the Java classpath using the \<^verbatim>\<open>classpath\<close> Bash function that is provided |
|
69 |
by the Isabelle process environment. Thus add-on components can register |
|
70 |
themselves in a modular manner, see also \secref{sec:components}. |
|
47825 | 71 |
|
61575 | 72 |
Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for adding |
73 |
plugin components, which needs special attention since it overrides the |
|
74 |
standard Java class loader. |
|
75 |
\<close> |
|
47825 | 76 |
|
52116
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
77 |
|
58618 | 78 |
section \<open>Scala script wrapper\<close> |
52116
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
79 |
|
61575 | 80 |
text \<open> |
81 |
The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"} |
|
82 |
allows to run Isabelle/Scala source files stand-alone programs, by using a |
|
62415 | 83 |
suitable ``hash-bang'' line and executable file permissions. For example: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
58618
diff
changeset
|
84 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
58618
diff
changeset
|
85 |
\<open>#!/usr/bin/env isabelle_scala_script |
52116
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
86 |
|
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
87 |
val options = isabelle.Options.init() |
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
88 |
Console.println("browser_info = " + options.bool("browser_info")) |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
58618
diff
changeset
|
89 |
Console.println("document = " + options.string("document"))\<close>} |
52116
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
90 |
|
62415 | 91 |
This assumes that the executable may be found via the @{setting PATH} from |
92 |
the process environment: this is the case when Isabelle settings are active, |
|
93 |
e.g.\ in the context of the main Isabelle tool wrapper |
|
63680 | 94 |
\secref{sec:isabelle-tool}. Alternatively, the full |
95 |
\<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded |
|
62415 | 96 |
form. |
61575 | 97 |
\<close> |
52116
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
48985
diff
changeset
|
98 |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
99 |
|
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
100 |
section \<open>Project setup for common Scala IDEs\<close> |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
101 |
|
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
102 |
text \<open> |
71389 | 103 |
The @{tool_def scala_project} tool creates a project configuration for |
104 |
Isabelle/Scala/jEdit: |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
105 |
@{verbatim [display] |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
106 |
\<open>Usage: isabelle scala_project [OPTIONS] PROJECT_DIR |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
107 |
|
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
108 |
Options are: |
71503 | 109 |
-L make symlinks to original scala files |
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
110 |
|
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
111 |
Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
112 |
such as IntelliJ IDEA.\<close>} |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
113 |
|
71389 | 114 |
The generated configuration is for Gradle\<^footnote>\<open>\<^url>\<open>https://gradle.org\<close>\<close>, but the |
115 |
main purpose is to import it into common Scala IDEs, such as IntelliJ |
|
116 |
IDEA\<^footnote>\<open>\<^url>\<open>https://www.jetbrains.com/idea\<close>\<close>. This allows to explore the |
|
117 |
sources with static analysis and other hints in real-time. |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
118 |
|
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
119 |
The specified project directory must not exist yet. The generated files |
71389 | 120 |
refer to physical file-system locations, using the path notation of the |
121 |
underlying OS platform. Thus the project needs to be recreated whenever the |
|
122 |
Isabelle installation is changed or moved. |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
123 |
|
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
124 |
\<^medskip> By default, Scala sources are \<^emph>\<open>copied\<close> from the Isabelle distribution and |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
125 |
editing them within the IDE has no permanent effect. |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
126 |
|
71523 | 127 |
Option \<^verbatim>\<open>-L\<close> produces \<^emph>\<open>symlinks\<close> to the original files: this allows to |
71389 | 128 |
develop Isabelle/Scala/jEdit within an external Scala IDE. Note that |
129 |
building the result always requires \<^verbatim>\<open>isabelle jedit -b\<close> on the |
|
130 |
command-line. |
|
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
131 |
\<close> |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
63680
diff
changeset
|
132 |
|
47825 | 133 |
end |