more Haskell operations;

--- a/src/Tools/Haskell/Haskell.thy	Tue Nov 06 14:30:53 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Tue Nov 06 14:53:56 2018 +0100
@@ -238,6 +238,9 @@
 
   lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
 
+  markupN, consistentN, unbreakableN, indentN, widthN,
+  blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
+
   wordsN, words, no_wordsN, no_words,
 
   tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
@@ -261,10 +264,11 @@
   Output, no_output)
 where
 
-import Prelude hiding (words, error)
+import Prelude hiding (words, error, break)
 
 import Isabelle.Library
 import qualified Isabelle.Properties as Properties
+import qualified Isabelle.Value as Value
 
 
 {- basic markup -}
@@ -321,6 +325,40 @@
 (positionN, position) = markup_elem \<open>Markup.positionN\<close>
 
 
+{- pretty printing -}
+
+markupN, consistentN, unbreakableN, indentN :: String
+markupN = \<open>Markup.markupN\<close>;
+consistentN = \<open>Markup.consistentN\<close>;
+unbreakableN = \<open>Markup.unbreakableN\<close>;
+indentN = \<open>Markup.indentN\<close>;
+
+widthN :: String
+widthN = \<open>Markup.widthN\<close>
+
+blockN :: String
+blockN = \<open>Markup.blockN\<close>
+block :: Bool -> Int -> T
+block c i =
+  (blockN,
+    (if c then [(consistentN, Value.print_bool c)] else []) ++
+    (if i /= 0 then [(indentN, Value.print_int i)] else []))
+
+breakN :: String
+breakN = \<open>Markup.breakN\<close>
+break :: Int -> Int -> T
+break w i =
+  (breakN,
+    (if w /= 0 then [(widthN, Value.print_int w)] else []) ++
+    (if i /= 0 then [(indentN, Value.print_int i)] else []))
+
+fbreakN :: String; fbreak :: T
+(fbreakN, fbreak) = markup_elem \<open>Markup.fbreakN\<close>
+
+itemN :: String; item :: T
+(itemN, item) = markup_elem \<open>Markup.itemN\<close>
+
+
 {- text properties -}
 
 wordsN :: String; words :: T
@@ -748,6 +786,158 @@
 variant _ _ = err_body
 \<close>
 
+generate_haskell_file "Pretty.hs" = \<open>
+{-  Title:      Tools/Haskell/Pretty.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Generic pretty printing module.
+-}
+
+module Isabelle.Pretty (
+  T, symbolic, formatted, unformatted,
+
+  str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
+  item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
+  commas, enclose, enum, list, str_list, big_list)
+where
+
+import Isabelle.Library hiding (quote)
+import qualified Data.List as List
+import qualified Isabelle.Buffer as Buffer
+import qualified Isabelle.Markup as Markup
+import qualified Isabelle.XML as XML
+import qualified Isabelle.YXML as YXML
+
+
+data T =
+    Block Markup.T Bool Int [T]
+  | Break Int Int
+  | Str String
+
+
+{- output -}
+
+output_spaces n = replicate n ' '
+
+symbolic_text "" = []
+symbolic_text s = [XML.Text s]
+
+symbolic_markup markup body =
+  if Markup.is_empty markup then body
+  else [XML.Elem markup body]
+
+symbolic :: T -> XML.Body
+symbolic (Block markup consistent indent prts) =
+  concatMap symbolic prts
+  |> symbolic_markup block_markup
+  |> symbolic_markup markup
+  where block_markup = if null prts then Markup.empty else Markup.block consistent indent
+symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind) (symbolic_text (output_spaces wd))]
+symbolic (Str s) = symbolic_text s
+
+formatted :: T -> String
+formatted = YXML.string_of_body . symbolic
+
+unformatted :: T -> String
+unformatted prt = Buffer.empty |> out prt |> Buffer.content
+  where
+    out (Block markup _ _ prts) =
+      let (bg, en) = YXML.output_markup markup
+      in Buffer.add bg #> fold out prts #> Buffer.add en
+    out (Break _ wd) = Buffer.add (output_spaces wd)
+    out (Str s) = Buffer.add s
+
+
+{- derived operations to create formatting expressions -}
+
+force_nat n | n < 0 = 0
+force_nat n = n
+
+str :: String -> T
+str = Str
+
+brk_indent :: Int -> Int -> T
+brk_indent wd ind = Break (force_nat wd) ind
+
+brk :: Int -> T
+brk wd = brk_indent wd 0
+
+fbrk :: T
+fbrk = str "\n"
+
+breaks, fbreaks :: [T] -> [T]
+breaks = List.intersperse (brk 1)
+fbreaks = List.intersperse fbrk
+
+blk :: (Int, [T]) -> T
+blk (indent, es) = Block Markup.empty False (force_nat indent) es
+
+block :: [T] -> T
+block prts = blk (2, prts)
+
+strs :: [String] -> T
+strs = block . breaks . map str
+
+markup :: Markup.T -> [T] -> T
+markup m = Block m False 0
+
+mark :: Markup.T -> T -> T
+mark m prt = if m == Markup.empty then prt else markup m [prt]
+
+mark_str :: (Markup.T, String) -> T
+mark_str (m, s) = mark m (str s)
+
+marks_str :: ([Markup.T], String) -> T
+marks_str (ms, s) = fold_rev mark ms (str s)
+
+item :: [T] -> T
+item = markup Markup.item
+
+text_fold :: [T] -> T
+text_fold = markup Markup.text_fold
+
+keyword1, keyword2 :: String -> T
+keyword1 name = mark_str (Markup.keyword1, name)
+keyword2 name = mark_str (Markup.keyword2, name)
+
+text :: String -> [T]
+text = breaks . map str . words
+
+paragraph :: [T] -> T
+paragraph = markup Markup.paragraph
+
+para :: String -> T
+para = paragraph . text
+
+quote :: T -> T
+quote prt = blk (1, [str "\"", prt, str "\""])
+
+cartouche :: T -> T
+cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"])
+
+separate :: String -> [T] -> [T]
+separate sep = List.intercalate [str sep, brk 1] . map single
+
+commas :: [T] -> [T]
+commas = separate ","
+
+enclose :: String -> String -> [T] -> T
+enclose lpar rpar prts = block (str lpar : prts ++ [str rpar])
+
+enum :: String -> String -> String -> [T] -> T
+enum sep lpar rpar = enclose lpar rpar . separate sep
+
+list :: String -> String -> [T] -> T
+list = enum ","
+
+str_list :: String -> String -> [String] -> T
+str_list lpar rpar = list lpar rpar . map str
+
+big_list :: String -> [T] -> T
+big_list name prts = block (fbreaks (str name : prts))
+\<close>
+
 generate_haskell_file "YXML.hs" = \<open>
 {-  Title:      Tools/Haskell/YXML.hs
     Author:     Makarius
@@ -757,7 +947,7 @@
 inlining into plain text.
 -}
 
-module Isabelle.YXML (charX, charY, strX, strY, detect,
+module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
   buffer_body, buffer, string_of_body, string_of, parse_body, parse)
 where
 
@@ -788,6 +978,11 @@
 
 {- output -}
 
+output_markup :: Markup.T -> Markup.Output
+output_markup markup@(name, atts) =
+  if Markup.is_empty markup then Markup.no_output
+  else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX)
+
 buffer_attrib (a, x) =
   Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
 

--- a/src/Tools/Haskell/Markup.hs	Tue Nov 06 14:30:53 2018 +0100
+++ b/src/Tools/Haskell/Markup.hs	Tue Nov 06 14:53:56 2018 +0100
@@ -14,6 +14,9 @@
 
   lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
 
+  markupN, consistentN, unbreakableN, indentN, widthN,
+  blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
+
   wordsN, words, no_wordsN, no_words,
 
   tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
@@ -37,10 +40,11 @@
   Output, no_output)
 where
 
-import Prelude hiding (words, error)
+import Prelude hiding (words, error, break)
 
 import Isabelle.Library
 import qualified Isabelle.Properties as Properties
+import qualified Isabelle.Value as Value
 
 
 {- basic markup -}
@@ -97,6 +101,40 @@
 (positionN, position) = markup_elem "position"
 
 
+{- pretty printing -}
+
+markupN, consistentN, unbreakableN, indentN :: String
+markupN = "markup";
+consistentN = "consistent";
+unbreakableN = "unbreakable";
+indentN = "indent";
+
+widthN :: String
+widthN = "width"
+
+blockN :: String
+blockN = "block"
+block :: Bool -> Int -> T
+block c i =
+  (blockN,
+    (if c then [(consistentN, Value.print_bool c)] else []) ++
+    (if i /= 0 then [(indentN, Value.print_int i)] else []))
+
+breakN :: String
+breakN = "break"
+break :: Int -> Int -> T
+break w i =
+  (breakN,
+    (if w /= 0 then [(widthN, Value.print_int w)] else []) ++
+    (if i /= 0 then [(indentN, Value.print_int i)] else []))
+
+fbreakN :: String; fbreak :: T
+(fbreakN, fbreak) = markup_elem "fbreak"
+
+itemN :: String; item :: T
+(itemN, item) = markup_elem "item"
+
+
 {- text properties -}
 
 wordsN :: String; words :: T

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Haskell/Pretty.hs	Tue Nov 06 14:53:56 2018 +0100
@@ -0,0 +1,151 @@
+{- generated by Isabelle -}
+
+{-  Title:      Tools/Haskell/Pretty.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Generic pretty printing module.
+-}
+
+module Isabelle.Pretty (
+  T, symbolic, formatted, unformatted,
+
+  str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
+  item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
+  commas, enclose, enum, list, str_list, big_list)
+where
+
+import Isabelle.Library hiding (quote)
+import qualified Data.List as List
+import qualified Isabelle.Buffer as Buffer
+import qualified Isabelle.Markup as Markup
+import qualified Isabelle.XML as XML
+import qualified Isabelle.YXML as YXML
+
+
+data T =
+    Block Markup.T Bool Int [T]
+  | Break Int Int
+  | Str String
+
+
+{- output -}
+
+output_spaces n = replicate n ' '
+
+symbolic_text "" = []
+symbolic_text s = [XML.Text s]
+
+symbolic_markup markup body =
+  if Markup.is_empty markup then body
+  else [XML.Elem markup body]
+
+symbolic :: T -> XML.Body
+symbolic (Block markup consistent indent prts) =
+  concatMap symbolic prts
+  |> symbolic_markup block_markup
+  |> symbolic_markup markup
+  where block_markup = if null prts then Markup.empty else Markup.block consistent indent
+symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind) (symbolic_text (output_spaces wd))]
+symbolic (Str s) = symbolic_text s
+
+formatted :: T -> String
+formatted = YXML.string_of_body . symbolic
+
+unformatted :: T -> String
+unformatted prt = Buffer.empty |> out prt |> Buffer.content
+  where
+    out (Block markup _ _ prts) =
+      let (bg, en) = YXML.output_markup markup
+      in Buffer.add bg #> fold out prts #> Buffer.add en
+    out (Break _ wd) = Buffer.add (output_spaces wd)
+    out (Str s) = Buffer.add s
+
+
+{- derived operations to create formatting expressions -}
+
+force_nat n | n < 0 = 0
+force_nat n = n
+
+str :: String -> T
+str = Str
+
+brk_indent :: Int -> Int -> T
+brk_indent wd ind = Break (force_nat wd) ind
+
+brk :: Int -> T
+brk wd = brk_indent wd 0
+
+fbrk :: T
+fbrk = str "\n"
+
+breaks, fbreaks :: [T] -> [T]
+breaks = List.intersperse (brk 1)
+fbreaks = List.intersperse fbrk
+
+blk :: (Int, [T]) -> T
+blk (indent, es) = Block Markup.empty False (force_nat indent) es
+
+block :: [T] -> T
+block prts = blk (2, prts)
+
+strs :: [String] -> T
+strs = block . breaks . map str
+
+markup :: Markup.T -> [T] -> T
+markup m = Block m False 0
+
+mark :: Markup.T -> T -> T
+mark m prt = if m == Markup.empty then prt else markup m [prt]
+
+mark_str :: (Markup.T, String) -> T
+mark_str (m, s) = mark m (str s)
+
+marks_str :: ([Markup.T], String) -> T
+marks_str (ms, s) = fold_rev mark ms (str s)
+
+item :: [T] -> T
+item = markup Markup.item
+
+text_fold :: [T] -> T
+text_fold = markup Markup.text_fold
+
+keyword1, keyword2 :: String -> T
+keyword1 name = mark_str (Markup.keyword1, name)
+keyword2 name = mark_str (Markup.keyword2, name)
+
+text :: String -> [T]
+text = breaks . map str . words
+
+paragraph :: [T] -> T
+paragraph = markup Markup.paragraph
+
+para :: String -> T
+para = paragraph . text
+
+quote :: T -> T
+quote prt = blk (1, [str "\"", prt, str "\""])
+
+cartouche :: T -> T
+cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"])
+
+separate :: String -> [T] -> [T]
+separate sep = List.intercalate [str sep, brk 1] . map single
+
+commas :: [T] -> [T]
+commas = separate ","
+
+enclose :: String -> String -> [T] -> T
+enclose lpar rpar prts = block (str lpar : prts ++ [str rpar])
+
+enum :: String -> String -> String -> [T] -> T
+enum sep lpar rpar = enclose lpar rpar . separate sep
+
+list :: String -> String -> [T] -> T
+list = enum ","
+
+str_list :: String -> String -> [String] -> T
+str_list lpar rpar = list lpar rpar . map str
+
+big_list :: String -> [T] -> T
+big_list name prts = block (fbreaks (str name : prts))

--- a/src/Tools/Haskell/YXML.hs	Tue Nov 06 14:30:53 2018 +0100
+++ b/src/Tools/Haskell/YXML.hs	Tue Nov 06 14:53:56 2018 +0100
@@ -8,7 +8,7 @@
 inlining into plain text.
 -}
 
-module Isabelle.YXML (charX, charY, strX, strY, detect,
+module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
   buffer_body, buffer, string_of_body, string_of, parse_body, parse)
 where
 
@@ -39,6 +39,11 @@
 
 {- output -}
 
+output_markup :: Markup.T -> Markup.Output
+output_markup markup@(name, atts) =
+  if Markup.is_empty markup then Markup.no_output
+  else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX)
+
 buffer_attrib (a, x) =
   Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
 

--- a/src/Tools/Haskell/haskell.ML	Tue Nov 06 14:30:53 2018 +0100
+++ b/src/Tools/Haskell/haskell.ML	Tue Nov 06 14:53:56 2018 +0100
@@ -56,6 +56,7 @@
   \<^path>\<open>XML/Encode.hs\<close>,
   \<^path>\<open>XML/Decode.hs\<close>,
   \<^path>\<open>YXML.hs\<close>,
+  \<^path>\<open>Pretty.hs\<close>,
   \<^path>\<open>Term.hs\<close>,
   \<^path>\<open>Term_XML/Encode.hs\<close>,
   \<^path>\<open>Term_XML/Decode.hs\<close>];