# HG changeset patch # User wenzelm # Date 1541513190 -3600 # Node ID 27423819534c89322337794d004adbdc71b7b9df # Parent c1fe9dcc274a2a8590ec17f8f48e0e8c7661dcbc# Parent 9f21381600e380ca1804cba6425e980e2573325b merged diff -r c1fe9dcc274a -r 27423819534c src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Sun Nov 04 15:00:30 2018 +0000 +++ b/src/Pure/General/pretty.ML Tue Nov 06 15:06:30 2018 +0100 @@ -326,10 +326,10 @@ (*unformatted output*) fun unformatted prt = let - fun fmt (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en - | fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd) - | fmt (Str (s, _)) = Buffer.add s; - in fmt prt Buffer.empty end; + fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en + | out (Break (_, wd, _)) = Buffer.add (output_spaces wd) + | out (Str (s, _)) = Buffer.add s; + in out prt Buffer.empty end; (* output interfaces *) diff -r c1fe9dcc274a -r 27423819534c src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Sun Nov 04 15:00:30 2018 +0000 +++ b/src/Tools/Haskell/Haskell.thy Tue Nov 06 15:06:30 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 \Markup.positionN\ +{- pretty printing -} + +markupN, consistentN, unbreakableN, indentN :: String +markupN = \Markup.markupN\; +consistentN = \Markup.consistentN\; +unbreakableN = \Markup.unbreakableN\; +indentN = \Markup.indentN\; + +widthN :: String +widthN = \Markup.widthN\ + +blockN :: String +blockN = \Markup.blockN\ +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 = \Markup.breakN\ +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 \Markup.fbreakN\ + +itemN :: String; item :: T +(itemN, item) = markup_elem \Markup.itemN\ + + {- text properties -} wordsN :: String; words :: T @@ -748,6 +786,158 @@ variant _ _ = err_body \ +generate_haskell_file "Pretty.hs" = \ +{- 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", prt, str "\92"]) + +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)) +\ + generate_haskell_file "YXML.hs" = \ {- 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 diff -r c1fe9dcc274a -r 27423819534c src/Tools/Haskell/Markup.hs --- a/src/Tools/Haskell/Markup.hs Sun Nov 04 15:00:30 2018 +0000 +++ b/src/Tools/Haskell/Markup.hs Tue Nov 06 15:06:30 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 diff -r c1fe9dcc274a -r 27423819534c src/Tools/Haskell/Pretty.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Haskell/Pretty.hs Tue Nov 06 15:06:30 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", prt, str "\92"]) + +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)) diff -r c1fe9dcc274a -r 27423819534c src/Tools/Haskell/YXML.hs --- a/src/Tools/Haskell/YXML.hs Sun Nov 04 15:00:30 2018 +0000 +++ b/src/Tools/Haskell/YXML.hs Tue Nov 06 15:06:30 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 diff -r c1fe9dcc274a -r 27423819534c src/Tools/Haskell/haskell.ML --- a/src/Tools/Haskell/haskell.ML Sun Nov 04 15:00:30 2018 +0000 +++ b/src/Tools/Haskell/haskell.ML Tue Nov 06 15:06:30 2018 +0100 @@ -56,6 +56,7 @@ \<^path>\XML/Encode.hs\, \<^path>\XML/Decode.hs\, \<^path>\YXML.hs\, + \<^path>\Pretty.hs\, \<^path>\Term.hs\, \<^path>\Term_XML/Encode.hs\, \<^path>\Term_XML/Decode.hs\];