# HG changeset patch
# User wenzelm
# Date 1590582442 -7200
# Node ID 1529336eaedc7a8e2d5956fd8b80c62c1d38a033
# Parent  0408f6814224730c1ef094b2774a93096876253d
check bash functions against Isabelle settings environment;

diff -r 0408f6814224 -r 1529336eaedc NEWS
--- a/NEWS	Wed May 27 13:57:13 2020 +0200
+++ b/NEWS	Wed May 27 14:27:22 2020 +0200
@@ -7,6 +7,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** Document preparation ***
+
+* Antiquotation @{bash_function NAME} prints the given GNU bash function
+verbatim --- checked against the Isabelle settings environment.
+
+
 *** Pure ***
 
 * Definitions in locales produce rule which can be added as congruence
diff -r 0408f6814224 -r 1529336eaedc etc/symbols
--- a/etc/symbols	Wed May 27 13:57:13 2020 +0200
+++ b/etc/symbols	Wed May 27 14:27:22 2020 +0200
@@ -417,6 +417,7 @@
 \<^plugin>              argument: cartouche
 \<^print>
 \<^prop>                argument: cartouche
+\<^bash_function>       argument: cartouche
 \<^scala>               argument: cartouche
 \<^scala_function>      argument: cartouche
 \<^scala_method>        argument: cartouche
diff -r 0408f6814224 -r 1529336eaedc src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Wed May 27 13:57:13 2020 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Wed May 27 14:27:22 2020 +0200
@@ -108,6 +108,7 @@
     @{antiquotation_def emph} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def bold} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def verbatim} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def bash_function} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def system_option} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def session} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\
@@ -199,6 +200,7 @@
       @@{antiquotation emph} options @{syntax text} |
       @@{antiquotation bold} options @{syntax text} |
       @@{antiquotation verbatim} options @{syntax text} |
+      @@{antiquotation bash_function} options @{syntax embedded} |
       @@{antiquotation system_option} options @{syntax embedded} |
       @@{antiquotation session} options @{syntax embedded} |
       @@{antiquotation path} options @{syntax embedded} |
@@ -292,6 +294,10 @@
   \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
   characters, using some type-writer font style.
 
+  \<^descr> \<open>@{bash_function name}\<close> prints the given GNU bash function verbatim. The
+  name is checked wrt.\ the Isabelle system environment @{cite
+  "isabelle-system"}.
+
   \<^descr> \<open>@{system_option name}\<close> prints the given system option verbatim. The name
   is checked wrt.\ cumulative \<^verbatim>\<open>etc/options\<close> of all Isabelle components,
   notably \<^file>\<open>~~/etc/options\<close>.
diff -r 0408f6814224 -r 1529336eaedc src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed May 27 13:57:13 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed May 27 14:27:22 2020 +0200
@@ -68,6 +68,7 @@
   val export_pathN: string val export_path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
+  val bash_functionN: string val bash_function: string -> T
   val scala_functionN: string val scala_function: string -> T
   val markupN: string
   val consistentN: string
@@ -406,6 +407,7 @@
 val (export_pathN, export_path) = markup_string "export_path" nameN;
 val (urlN, url) = markup_string "url" nameN;
 val (docN, doc) = markup_string "doc" nameN;
+val (bash_functionN, bash_function) = markup_string "bash_function" nameN;
 val (scala_functionN, scala_function) = markup_string "scala_function" nameN;
 
 
diff -r 0408f6814224 -r 1529336eaedc src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Wed May 27 13:57:13 2020 +0200
+++ b/src/Pure/System/isabelle_system.ML	Wed May 27 14:27:22 2020 +0200
@@ -6,6 +6,11 @@
 
 signature ISABELLE_SYSTEM =
 sig
+  val bash_output_check: string -> string
+  val bash_output: string -> string * int
+  val bash: string -> int
+  val bash_functions: unit -> string list
+  val check_bash_function: Proof.context -> string * Position.T -> string
   val rm_tree: Path.T -> unit
   val mkdirs: Path.T -> unit
   val mkdir: Path.T -> unit
@@ -15,9 +20,6 @@
   val create_tmp_path: string -> string -> Path.T
   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
-  val bash_output_check: string -> string
-  val bash_output: string -> string * int
-  val bash: string -> int
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
@@ -43,6 +45,31 @@
   in rc end;
 
 
+(* bash functions *)
+
+fun bash_functions () =
+  bash_output_check "declare -Fx"
+  |> split_lines |> map_filter (space_explode " " #> try List.last);
+
+fun check_bash_function ctxt (name, pos) =
+  let
+    val kind = Markup.bash_functionN;
+    val funs = bash_functions ();
+  in
+    if member (op =) funs name then
+      (Context_Position.report ctxt pos (Markup.bash_function name); name)
+    else
+      let
+        val completion_report =
+          Completion.make_report (name, pos)
+            (fn completed =>
+              filter completed funs
+              |> sort_strings
+              |> map (fn a => (a, (kind, a))));
+      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end
+  end;
+
+
 (* directory operations *)
 
 fun system_command cmd =
diff -r 0408f6814224 -r 1529336eaedc src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Wed May 27 13:57:13 2020 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Wed May 27 14:27:22 2020 +0200
@@ -260,6 +260,13 @@
       in #1 (Input.source_content text) end));
 
 
+(* bash functions *)
+
+val _ = Theory.setup
+  (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>bash_function\<close>
+    (Scan.lift Args.embedded_position) Isabelle_System.check_bash_function);
+
+
 (* system options *)
 
 val _ = Theory.setup