added GHC.read_source: read Haskell source text with antiquotations;
added "cartouche" antiquotation for ML string expressions as Haskell string literals;

--- a/NEWS	Tue Oct 30 19:25:32 2018 +0100
+++ b/NEWS	Tue Oct 30 22:05:30 2018 +0100
@@ -87,6 +87,22 @@
 potentially with variations on ML syntax (existing ML_Env.SML_operations
 observes the official standard).
 
+* GHC.read_source reads Haskell source text with antiquotations (only
+the control-cartouche form). The default "cartouche" antiquotation
+evaluates an ML expression of type string and inlines the result as
+Haskell string literal. This allows to refer to Isabelle items robustly,
+e.g. via Isabelle/ML antiquotations or library operations. For example:
+
+ML \<open>
+  GHC.read_source \<^context> \<open>
+    allConst, impConst, eqConst :: String
+    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
+    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
+    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
+  \<close>
+  |> File.write \<^path>\<open>consts.hs\<close>
+\<close>
+
 
 *** System ***
 

--- a/src/Pure/PIDE/markup.ML	Tue Oct 30 19:25:32 2018 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Oct 30 22:05:30 2018 +0100
@@ -31,6 +31,7 @@
   val language_prop: bool -> T
   val language_ML: bool -> T
   val language_SML: bool -> T
+  val language_haskell: bool -> T
   val language_document: bool -> T
   val language_antiquotation: T
   val language_text: bool -> T
@@ -118,6 +119,7 @@
   val antiquotedN: string val antiquoted: T
   val antiquoteN: string val antiquote: T
   val ML_antiquotationN: string
+  val haskell_antiquotationN: string
   val document_antiquotationN: string
   val document_antiquotation_optionN: string
   val paragraphN: string val paragraph: T
@@ -302,6 +304,7 @@
 val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
 val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
 val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
+val language_haskell = language' {name = "Haskell", symbols = false, antiquotes = true};
 val language_document = language' {name = "document", symbols = false, antiquotes = true};
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
@@ -477,6 +480,7 @@
 val (antiquoteN, antiquote) = markup_elem "antiquote";
 
 val ML_antiquotationN = "ML_antiquotation";
+val haskell_antiquotationN = "Haskell_antiquotation";
 val document_antiquotationN = "document_antiquotation";
 val document_antiquotation_optionN = "document_antiquotation_option";
 

--- a/src/Pure/Tools/ghc.ML	Tue Oct 30 19:25:32 2018 +0100
+++ b/src/Pure/Tools/ghc.ML	Tue Oct 30 22:05:30 2018 +0100
@@ -9,6 +9,10 @@
   val print_codepoint: UTF8.codepoint -> string
   val print_symbol: Symbol.symbol -> string
   val print_string: string -> string
+  val antiquotation: binding -> 'a Token.context_parser ->
+    ({context: Proof.context, source: Token.src, argument: 'a} -> string) -> theory -> theory
+  val read_source: Proof.context -> Input.source -> string
+  val set_result: string -> Proof.context -> Proof.context
 end;
 
 structure GHC: GHC =
@@ -42,4 +46,82 @@
 
 val print_string = quote o implode o map print_symbol o Symbol.explode;
 
+
+(** antiquotations **)
+
+(* theory data *)
+
+structure Antiqs = Theory_Data
+(
+  type T = (Token.src -> Proof.context -> string) Name_Space.table;
+  val empty : T = Name_Space.empty_table Markup.haskell_antiquotationN;
+  val extend = I;
+  fun merge tabs : T = Name_Space.merge_tables tabs;
+);
+
+val get_antiquotations = Antiqs.get o Proof_Context.theory_of;
+
+fun antiquotation name scan body thy =
+  let
+    fun antiq src ctxt =
+      let val (x, ctxt') = Token.syntax scan src ctxt
+      in body {context = ctxt', source = src, argument = x} end;
+  in thy |> Antiqs.map (Name_Space.define (Context.Theory thy) true (name, antiq) #> #2) end;
+
+
+(* read source and expand antiquotations *)
+
+val scan_antiq =
+  Antiquote.scan_control >> Antiquote.Control ||
+  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
+
+fun read_source ctxt source =
+  let
+    val _ =
+      Context_Position.report ctxt (Input.pos_of source)
+        (Markup.language_haskell (Input.is_delimited source));
+
+    val (input, _) =
+      Input.source_explode source
+      |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq));
+
+    val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input);
+
+    fun expand antiq =
+      (case antiq of
+        Antiquote.Text s => s
+      | Antiquote.Control {name, body, ...} =>
+          let
+            val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]);
+            val (src', f) = Token.check_src ctxt get_antiquotations src;
+          in f src' ctxt end
+      | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq))));
+  in implode (map expand input) end;
+
+
+(* concrete antiquotation: ML expression as Haskell string literal *)
+
+structure Local_Data = Proof_Data
+(
+  type T = string option;
+  fun init _ = NONE;
+);
+
+val set_result = Local_Data.put o SOME;
+
+fun the_result ctxt =
+  (case Local_Data.get ctxt of
+    SOME s => s
+  | NONE => raise Fail "No result");
+
+val _ =
+  Theory.setup
+    (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
+      (fn {context = ctxt, argument, ...} =>
+        ctxt |> Context.proof_map
+          (ML_Context.expression ("result", Position.thread_data ())
+            "string" "Context.map_proof (GHC.set_result result)"
+            (ML_Lex.read_source argument))
+        |> the_result |> print_string));
+
 end;