more ML antiquotations;
authorwenzelm
Fri Dec 14 11:43:48 2018 +0100 (11 months ago)
changeset 69470c8c3285f1294
parent 69469 95494ec22c71
child 69471 e7fd8c6d183a
more ML antiquotations;
NEWS
src/Pure/ML/ml_antiquotation.ML
src/Pure/Tools/ghc.ML
     1.1 --- a/NEWS	Fri Dec 14 11:35:58 2018 +0100
     1.2 +++ b/NEWS	Fri Dec 14 11:43:48 2018 +0100
     1.3 @@ -122,6 +122,10 @@
     1.4  * ML antiquotation @{master_dir} refers to the master directory of the
     1.5  underlying theory, i.e. the directory of the theory file.
     1.6  
     1.7 +* ML antiquotation @{verbatim} inlines its argument as string literal,
     1.8 +preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly
     1.9 +useful.
    1.10 +
    1.11  * Command 'generate_file' allows to produce sources for other languages,
    1.12  with antiquotations in the Isabelle context (only the control-cartouche
    1.13  form). The default "cartouche" antiquotation evaluates an ML expression
     2.1 --- a/src/Pure/ML/ml_antiquotation.ML	Fri Dec 14 11:35:58 2018 +0100
     2.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Fri Dec 14 11:43:48 2018 +0100
     2.3 @@ -46,6 +46,9 @@
     2.4    value (Binding.make ("cartouche", \<^here>))
     2.5      (Scan.lift Args.cartouche_input >> (fn source =>
     2.6        "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
     2.7 -        ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
     2.8 +        ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>
     2.9 +
    2.10 +  inline (Binding.make ("verbatim", \<^here>))
    2.11 +    (Scan.lift Args.embedded >> ML_Syntax.print_string));
    2.12  
    2.13  end;
     3.1 --- a/src/Pure/Tools/ghc.ML	Fri Dec 14 11:35:58 2018 +0100
     3.2 +++ b/src/Pure/Tools/ghc.ML	Fri Dec 14 11:43:48 2018 +0100
     3.3 @@ -48,7 +48,7 @@
     3.4  (* project setup *)
     3.5  
     3.6  fun project_template {depends, modules} =
     3.7 -  Input.source_content_string \<open>{-# START_FILE {{name}}.cabal #-}
     3.8 +  \<^verbatim>\<open>{-# START_FILE {{name}}.cabal #-}
     3.9  name:                {{name}}
    3.10  version:             0.1.0.0
    3.11  homepage:            default
    3.12 @@ -64,9 +64,9 @@
    3.13    main-is:             Main.hs
    3.14    default-language:    Haskell2010
    3.15    build-depends:       \<close> ^ commas ("base >= 4.7 && < 5" :: depends) ^
    3.16 -  Input.source_content_string \<open>
    3.17 +  \<^verbatim>\<open>
    3.18    other-modules:       \<close> ^ commas modules ^
    3.19 -  Input.source_content_string \<open>
    3.20 +  \<^verbatim>\<open>
    3.21  {-# START_FILE Setup.hs #-}
    3.22  import Distribution.Simple
    3.23  main = defaultMain