# HG changeset patch
# User wenzelm
# Date 1544784228 -3600
# Node ID c8c3285f129414a868150233f642ff580b9b80c6
# Parent  95494ec22c711535c256a5e590b7367302aa777d
more ML antiquotations;

diff -r 95494ec22c71 -r c8c3285f1294 NEWS
--- a/NEWS	Fri Dec 14 11:35:58 2018 +0100
+++ b/NEWS	Fri Dec 14 11:43:48 2018 +0100
@@ -122,6 +122,10 @@
 * ML antiquotation @{master_dir} refers to the master directory of the
 underlying theory, i.e. the directory of the theory file.
 
+* ML antiquotation @{verbatim} inlines its argument as string literal,
+preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly
+useful.
+
 * Command 'generate_file' allows to produce sources for other languages,
 with antiquotations in the Isabelle context (only the control-cartouche
 form). The default "cartouche" antiquotation evaluates an ML expression
diff -r 95494ec22c71 -r c8c3285f1294 src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Fri Dec 14 11:35:58 2018 +0100
+++ b/src/Pure/ML/ml_antiquotation.ML	Fri Dec 14 11:43:48 2018 +0100
@@ -46,6 +46,9 @@
   value (Binding.make ("cartouche", \<^here>))
     (Scan.lift Args.cartouche_input >> (fn source =>
       "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
-        ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
+        ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>
+
+  inline (Binding.make ("verbatim", \<^here>))
+    (Scan.lift Args.embedded >> ML_Syntax.print_string));
 
 end;
diff -r 95494ec22c71 -r c8c3285f1294 src/Pure/Tools/ghc.ML
--- a/src/Pure/Tools/ghc.ML	Fri Dec 14 11:35:58 2018 +0100
+++ b/src/Pure/Tools/ghc.ML	Fri Dec 14 11:43:48 2018 +0100
@@ -48,7 +48,7 @@
 (* project setup *)
 
 fun project_template {depends, modules} =
-  Input.source_content_string \<open>{-# START_FILE {{name}}.cabal #-}
+  \<^verbatim>\<open>{-# START_FILE {{name}}.cabal #-}
 name:                {{name}}
 version:             0.1.0.0
 homepage:            default
@@ -64,9 +64,9 @@
   main-is:             Main.hs
   default-language:    Haskell2010
   build-depends:       \<close> ^ commas ("base >= 4.7 && < 5" :: depends) ^
-  Input.source_content_string \<open>
+  \<^verbatim>\<open>
   other-modules:       \<close> ^ commas modules ^
-  Input.source_content_string \<open>
+  \<^verbatim>\<open>
 {-# START_FILE Setup.hs #-}
 import Distribution.Simple
 main = defaultMain