more uniform output of source / text / theory_text, with handling of formal comments etc.;

--- a/src/Pure/Thy/document_antiquotation.ML	Fri Jan 19 15:20:13 2018 +0100
+++ b/src/Pure/Thy/document_antiquotation.ML	Fri Jan 19 19:09:25 2018 +0100
@@ -16,6 +16,7 @@
   val trim_blanks: Proof.context -> string -> string
   val trim_lines: Proof.context -> string -> string
   val indent_lines: Proof.context -> string -> string
+  val prepare_lines: Proof.context -> string -> string
   val quote: Proof.context -> Pretty.T -> Pretty.T
   val indent: Proof.context -> Pretty.T -> Pretty.T
   val format: Proof.context -> Pretty.T -> string
@@ -60,6 +61,8 @@
     prefix_lines (Symbol.spaces (Config.get ctxt thy_output_indent))
   else I;
 
+fun prepare_lines ctxt = trim_lines ctxt #> indent_lines ctxt;
+
 
 (* output *)
 

--- a/src/Pure/Thy/document_antiquotations.ML	Fri Jan 19 15:20:13 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Fri Jan 19 19:09:25 2018 +0100
@@ -150,51 +150,56 @@
 
 local
 
+fun report_text ctxt text =
+  Context_Position.report ctxt (Input.pos_of text)
+    (Markup.language_text (Input.is_delimited text));
+
+fun prepare_text ctxt =
+  Input.source_content #> Document_Antiquotation.prepare_lines ctxt;
+
 fun text_antiquotation name =
   Thy_Output.antiquotation_raw name (Scan.lift Args.text_input)
     (fn ctxt => fn text =>
       let
+        val _ = report_text ctxt text;
+      in
+        prepare_text ctxt text
+        |> Thy_Output.output_source ctxt
+        |> Thy_Output.isabelle ctxt
+      end);
+
+val theory_text_antiquotation =
+  Thy_Output.antiquotation_raw \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
+    (fn ctxt => fn text =>
+      let
+        val keywords = Thy_Header.get_keywords' ctxt;
+
+        val _ = report_text ctxt text;
         val _ =
-          Context_Position.report ctxt (Input.pos_of text)
-            (Markup.language_text (Input.is_delimited text));
-      in Thy_Output.pretty ctxt [Thy_Output.pretty_text ctxt (Input.source_content text)] end);
+          Input.source_explode text
+          |> Source.of_list
+          |> Token.source' true keywords
+          |> Source.exhaust
+          |> maps (Token.reports keywords)
+          |> Context_Position.reports_text ctxt;
+      in
+        prepare_text ctxt text
+        |> Token.explode keywords Position.none
+        |> maps (Thy_Output.output_token ctxt)
+        |> Thy_Output.isabelle ctxt
+      end);
 
 in
 
 val _ =
   Theory.setup
    (text_antiquotation \<^binding>\<open>text\<close> #>
-    text_antiquotation \<^binding>\<open>cartouche\<close>);
+    text_antiquotation \<^binding>\<open>cartouche\<close> #>
+    theory_text_antiquotation);
 
 end;
 
 
-(* theory text with tokens (unchecked) *)
-
-val _ =
-  Theory.setup
-    (Thy_Output.antiquotation_raw \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
-      (fn ctxt => fn text =>
-        let
-          val keywords = Thy_Header.get_keywords' ctxt;
-
-          val _ =
-            Context_Position.report ctxt (Input.pos_of text)
-              (Markup.language_Isar (Input.is_delimited text));
-          val _ =
-            Input.source_explode text
-            |> Source.of_list
-            |> Token.source' true keywords
-            |> Source.exhaust
-            |> maps (Token.reports keywords)
-            |> Context_Position.reports_text ctxt;
-
-          val toks =
-            Input.source_content text
-            |> Document_Antiquotation.trim_lines ctxt
-            |> Document_Antiquotation.indent_lines ctxt
-            |> Token.explode keywords Position.none;
-        in Thy_Output.isabelle ctxt (maps (Thy_Output.output_token ctxt) toks) end));
 
 
 (* goal state *)

--- a/src/Pure/Thy/thy_output.ML	Fri Jan 19 15:20:13 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Jan 19 19:09:25 2018 +0100
@@ -10,9 +10,9 @@
   val check_comments: Proof.context -> Symbol_Pos.T list -> unit
   val check_token_comments: Proof.context -> Token.T -> unit
   val output_token: Proof.context -> Token.T -> Latex.text list
+  val output_source: Proof.context -> string -> Latex.text list
   val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
     Token.T list -> Latex.text list
-  val pretty_text: Proof.context -> string -> Pretty.T
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val lines: Latex.text list -> Latex.text list
@@ -20,6 +20,7 @@
   val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
   val typewriter: Proof.context -> string -> Latex.text
   val verbatim: Proof.context -> string -> Latex.text
+  val source: Proof.context -> Token.src -> Latex.text
   val pretty: Proof.context -> Pretty.T list -> Latex.text
   val pretty_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
   val antiquotation_pretty:
@@ -133,6 +134,9 @@
     | _ => output false "" "")
   end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 
+fun output_source ctxt s =
+  output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none));
+
 fun check_comments ctxt =
   Comment.read_body #> (Option.app o List.app) (fn (comment, syms) =>
     let
@@ -430,9 +434,6 @@
 
 (* pretty printing *)
 
-fun pretty_text ctxt =
-  Pretty.chunks o map (Pretty.str o Document_Antiquotation.trim_blanks ctxt) o split_lines;
-
 fun pretty_term ctxt t =
   Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
 
@@ -461,13 +462,19 @@
   then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
   else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
 
+fun source ctxt =
+  Token.args_of_src
+  #> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt)
+  #> space_implode " "
+  #> output_source ctxt
+  #> isabelle ctxt;
+
 fun pretty ctxt =
   map (Document_Antiquotation.output ctxt #> Latex.string) #> lines #> isabelle ctxt;
 
 fun pretty_source ctxt src prts =
-  if Config.get ctxt Document_Antiquotation.thy_output_source then
-    pretty ctxt [pretty_text ctxt (space_implode " " (map Token.unparse (Token.args_of_src src)))]
-  else pretty ctxt prts;
+  if Config.get ctxt Document_Antiquotation.thy_output_source
+  then source ctxt src else pretty ctxt prts;
 
 
 (* antiquotation variants *)