--- 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
--- 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;
--- 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