# HG changeset patch
# User wenzelm
# Date 1539006163 -7200
# Node ID be20f5f6feb9d705f8d5528cb86924dc9ff24418
# Parent  a142ec271d83e5f1d9e3562e62a8608fc86fdd40
support for OCaml via command-line tools;

diff -r a142ec271d83 -r be20f5f6feb9 NEWS
--- a/NEWS	Mon Oct 08 12:52:28 2018 +0200
+++ b/NEWS	Mon Oct 08 15:42:43 2018 +0200
@@ -25,7 +25,6 @@
 (legacy feature since Isabelle2016).
 
 
-
 *** HOL ***
 
 * Simplified syntax setup for big operators under image. In rare
@@ -90,6 +89,12 @@
 presence of structurally broken sources: full consolidation of theories
 is no longer required.
 
+* Support for OCaml via command-line tools "isabelle ocaml_setup",
+"isabelle ocaml", "isabelle ocamlc", "isabelle ocaml_opam". Existing
+settings variables ISABELLE_OCAML and ISABELLE_OCAMLC are maintained
+dynamically according the state of ISABELLE_OPAM_ROOT concerning
+ISABELLE_OCAML_VERSION.
+
 
 
 New in Isabelle2018 (August 2018)
diff -r a142ec271d83 -r be20f5f6feb9 etc/settings
--- a/etc/settings	Mon Oct 08 12:52:28 2018 +0200
+++ b/etc/settings	Mon Oct 08 15:42:43 2018 +0200
@@ -138,6 +138,8 @@
 
 ISABELLE_OPAM_ROOT="$ISABELLE_HOME_USER/opam"
 
+ISABELLE_OCAML_VERSION="4.05.0"
+
 
 ###
 ### Misc settings
@@ -147,7 +149,5 @@
 
 #ISABELLE_GHC="/usr/bin/ghc"
 #ISABELLE_MLTON="/usr/bin/mlton"
-#ISABELLE_OCAML="/usr/bin/ocaml"
-#ISABELLE_OCAMLC="/usr/bin/ocamlc"
 #ISABELLE_SMLNJ="/usr/bin/sml"
 #ISABELLE_SWIPL="/usr/bin/swipl"
diff -r a142ec271d83 -r be20f5f6feb9 lib/Tools/ocaml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ocaml	Mon Oct 08 15:42:43 2018 +0200
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: invoke OCaml within the Isabelle environment
+
+isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocaml "$@"
diff -r a142ec271d83 -r be20f5f6feb9 lib/Tools/ocaml_opam
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ocaml_opam	Mon Oct 08 15:42:43 2018 +0200
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: invoke OCaml Package Manager within the Isabelle environment
+
+isabelle_opam "$@"
diff -r a142ec271d83 -r be20f5f6feb9 lib/Tools/ocaml_setup
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ocaml_setup	Mon Oct 08 15:42:43 2018 +0200
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: OCaml setup via OPAM
+
+isabelle_opam init --no-setup --compiler="$ISABELLE_OCAML_VERSION" "$@"
diff -r a142ec271d83 -r be20f5f6feb9 lib/Tools/ocamlc
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ocamlc	Mon Oct 08 15:42:43 2018 +0200
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: invoke OCaml compiler within the Isabelle environment
+
+isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocamlc "$@"
diff -r a142ec271d83 -r be20f5f6feb9 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Mon Oct 08 12:52:28 2018 +0200
+++ b/lib/scripts/getsettings	Mon Oct 08 15:42:43 2018 +0200
@@ -99,6 +99,14 @@
   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
 fi
 
+#OCaml
+if [ -z "$ISABELLE_OCAML" -a -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocaml" ]; then
+  ISABELLE_OCAML="$ISABELLE_HOME/lib/Tools/ocaml"
+fi
+if [ -z "$ISABELLE_OCAMLC" -a -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocamlc" ]; then
+  ISABELLE_OCAMLC="$ISABELLE_HOME/lib/Tools/ocamlc"
+fi
+
 #enforce JAVA_HOME
 if [ -d "$ISABELLE_JDK_HOME/jre" ]
 then