# HG changeset patch
# User wenzelm
# Date 1618607760 -7200
# Node ID 76d0b6597c910089b19a5d5e014e0ff7be4f9f2f
# Parent  386416437ce9026de2955413d316f3b8dd2854f3
support for conditional ML text;

diff -r 386416437ce9 -r 76d0b6597c91 NEWS
--- a/NEWS	Fri Apr 16 21:54:08 2021 +0200
+++ b/NEWS	Fri Apr 16 23:16:00 2021 +0200
@@ -92,6 +92,13 @@
 the given ML expression, in contrast to functions "try" and "can" that
 modify application of a function.
 
+* ML antiquotations for conditional ML text:
+
+    \<^if_linux>\<open>...\<close>
+    \<^if_macos>\<open>...\<close>
+    \<^if_windows>\<open>...\<close>
+    \<^if_unix>\<open>...\<close>
+
 * External bash processes are always managed by Isabelle/Scala, in
 contrast to Isabelle2021 where this was only done for macOS on Apple
 Silicon.
diff -r 386416437ce9 -r 76d0b6597c91 etc/symbols
--- a/etc/symbols	Fri Apr 16 21:54:08 2021 +0200
+++ b/etc/symbols	Fri Apr 16 23:16:00 2021 +0200
@@ -491,3 +491,8 @@
 \<^computation>         argument: cartouche
 \<^computation_conv>    argument: cartouche
 \<^computation_check>   argument: cartouche
+\<^if_linux>            argument: cartouche
+\<^if_macos>            argument: cartouche
+\<^if_windows>          argument: cartouche
+\<^if_unix>             argument: cartouche
+
diff -r 386416437ce9 -r 76d0b6597c91 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Fri Apr 16 21:54:08 2021 +0200
+++ b/lib/texinputs/isabellesym.sty	Fri Apr 16 23:16:00 2021 +0200
@@ -479,3 +479,7 @@
 \newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}}
 \newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}}
 \newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}}
+\newcommand{\isactrlifUNDERSCORElinux}{\isakeywordcontrol{if{\isacharunderscore}linux}}
+\newcommand{\isactrlifUNDERSCOREmacos}{\isakeywordcontrol{if{\isacharunderscore}macos}}
+\newcommand{\isactrlifUNDERSCOREwindows}{\isakeywordcontrol{if{\isacharunderscore}windows}}
+\newcommand{\isactrlifUNDERSCOREunix}{\isakeywordcontrol{if{\isacharunderscore}unix}}
diff -r 386416437ce9 -r 76d0b6597c91 src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Fri Apr 16 21:54:08 2021 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Fri Apr 16 23:16:00 2021 +0200
@@ -19,6 +19,7 @@
   val value: binding -> string context_parser -> theory -> theory
   val value_embedded: binding -> string context_parser -> theory -> theory
   val special_form: binding -> string -> theory -> theory
+  val conditional: binding -> (Proof.context -> bool) -> theory -> theory
 end;
 
 structure ML_Antiquotation: ML_ANTIQUOTATION =
@@ -64,7 +65,7 @@
 end;
 
 
-(* ML special form *)
+(* ML macros *)
 
 fun special_form binding operator =
   ML_Context.add_antiquotation binding true
@@ -85,6 +86,15 @@
           in (ml_env, ml_body') end;
       in (decl', ctxt') end);
 
+fun conditional binding check =
+  ML_Context.add_antiquotation binding true
+    (fn _ => fn src => fn ctxt =>
+      let val (s, _) = Token.syntax (Scan.lift Args.embedded_input) src ctxt in
+        if check ctxt then
+          ML_Context.expand_antiquotes (ML_Lex.read_source s) ctxt
+        else (K ([], []), ctxt)
+      end);
+
 
 (* basic antiquotations *)
 
diff -r 386416437ce9 -r 76d0b6597c91 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Fri Apr 16 21:54:08 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Fri Apr 16 23:16:00 2021 +0200
@@ -34,7 +34,12 @@
   ML_Antiquotation.value \<^binding>\<open>rat\<close>
     (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat --
       Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) =>
-        "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))))
+        "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))) #>
+
+  ML_Antiquotation.conditional \<^binding>\<open>if_linux\<close> (fn _ => ML_System.platform_is_linux) #>
+  ML_Antiquotation.conditional \<^binding>\<open>if_macos\<close> (fn _ => ML_System.platform_is_macos) #>
+  ML_Antiquotation.conditional \<^binding>\<open>if_windows\<close> (fn _ => ML_System.platform_is_windows) #>
+  ML_Antiquotation.conditional \<^binding>\<open>if_unix\<close> (fn _ => ML_System.platform_is_unix));
 
 
 (* formal entities *)
diff -r 386416437ce9 -r 76d0b6597c91 src/Pure/ML/ml_system.ML
--- a/src/Pure/ML/ml_system.ML	Fri Apr 16 21:54:08 2021 +0200
+++ b/src/Pure/ML/ml_system.ML	Fri Apr 16 23:16:00 2021 +0200
@@ -8,7 +8,10 @@
 sig
   val name: string
   val platform: string
+  val platform_is_linux: bool
+  val platform_is_macos: bool
   val platform_is_windows: bool
+  val platform_is_unix: bool
   val platform_is_64: bool
   val platform_is_arm: bool
   val platform_path: string -> string
@@ -20,7 +23,11 @@
 
 val SOME name = OS.Process.getEnv "ML_SYSTEM";
 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
+
+val platform_is_linux = String.isSuffix "linux" platform;
+val platform_is_macos = String.isSuffix "darwin" platform;
 val platform_is_windows = String.isSuffix "windows" platform;
+val platform_is_unix = platform_is_linux orelse platform_is_macos;
 val platform_is_64 = String.isPrefix "x86_64-" platform;
 val platform_is_arm = String.isPrefix "arm64-" platform;