1 {- generated by Isabelle -} |
|
2 |
|
3 {- Title: Tools/Haskell/Pretty.hs |
|
4 Author: Makarius |
|
5 LICENSE: BSD 3-clause (Isabelle) |
|
6 |
|
7 Generic pretty printing module. |
|
8 |
|
9 See also "$ISABELLE_HOME/src/Pure/General/pretty.ML". |
|
10 -} |
|
11 |
|
12 module Isabelle.Pretty ( |
|
13 T, symbolic, formatted, unformatted, |
|
14 |
|
15 str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str, |
|
16 item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate, |
|
17 commas, enclose, enum, list, str_list, big_list) |
|
18 where |
|
19 |
|
20 import Isabelle.Library hiding (quote) |
|
21 import qualified Data.List as List |
|
22 import qualified Isabelle.Buffer as Buffer |
|
23 import qualified Isabelle.Markup as Markup |
|
24 import qualified Isabelle.XML as XML |
|
25 import qualified Isabelle.YXML as YXML |
|
26 |
|
27 |
|
28 data T = |
|
29 Block Markup.T Bool Int [T] |
|
30 | Break Int Int |
|
31 | Str String |
|
32 |
|
33 |
|
34 {- output -} |
|
35 |
|
36 output_spaces n = replicate n ' ' |
|
37 |
|
38 symbolic_text "" = [] |
|
39 symbolic_text s = [XML.Text s] |
|
40 |
|
41 symbolic_markup markup body = |
|
42 if Markup.is_empty markup then body |
|
43 else [XML.Elem (markup, body)] |
|
44 |
|
45 symbolic :: T -> XML.Body |
|
46 symbolic (Block markup consistent indent prts) = |
|
47 concatMap symbolic prts |
|
48 |> symbolic_markup block_markup |
|
49 |> symbolic_markup markup |
|
50 where block_markup = if null prts then Markup.empty else Markup.block consistent indent |
|
51 symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind, symbolic_text (output_spaces wd))] |
|
52 symbolic (Str s) = symbolic_text s |
|
53 |
|
54 formatted :: T -> String |
|
55 formatted = YXML.string_of_body . symbolic |
|
56 |
|
57 unformatted :: T -> String |
|
58 unformatted prt = Buffer.empty |> out prt |> Buffer.content |
|
59 where |
|
60 out (Block markup _ _ prts) = |
|
61 let (bg, en) = YXML.output_markup markup |
|
62 in Buffer.add bg #> fold out prts #> Buffer.add en |
|
63 out (Break _ wd) = Buffer.add (output_spaces wd) |
|
64 out (Str s) = Buffer.add s |
|
65 |
|
66 |
|
67 {- derived operations to create formatting expressions -} |
|
68 |
|
69 force_nat n | n < 0 = 0 |
|
70 force_nat n = n |
|
71 |
|
72 str :: String -> T |
|
73 str = Str |
|
74 |
|
75 brk_indent :: Int -> Int -> T |
|
76 brk_indent wd ind = Break (force_nat wd) ind |
|
77 |
|
78 brk :: Int -> T |
|
79 brk wd = brk_indent wd 0 |
|
80 |
|
81 fbrk :: T |
|
82 fbrk = str "\n" |
|
83 |
|
84 breaks, fbreaks :: [T] -> [T] |
|
85 breaks = List.intersperse (brk 1) |
|
86 fbreaks = List.intersperse fbrk |
|
87 |
|
88 blk :: (Int, [T]) -> T |
|
89 blk (indent, es) = Block Markup.empty False (force_nat indent) es |
|
90 |
|
91 block :: [T] -> T |
|
92 block prts = blk (2, prts) |
|
93 |
|
94 strs :: [String] -> T |
|
95 strs = block . breaks . map str |
|
96 |
|
97 markup :: Markup.T -> [T] -> T |
|
98 markup m = Block m False 0 |
|
99 |
|
100 mark :: Markup.T -> T -> T |
|
101 mark m prt = if m == Markup.empty then prt else markup m [prt] |
|
102 |
|
103 mark_str :: (Markup.T, String) -> T |
|
104 mark_str (m, s) = mark m (str s) |
|
105 |
|
106 marks_str :: ([Markup.T], String) -> T |
|
107 marks_str (ms, s) = fold_rev mark ms (str s) |
|
108 |
|
109 item :: [T] -> T |
|
110 item = markup Markup.item |
|
111 |
|
112 text_fold :: [T] -> T |
|
113 text_fold = markup Markup.text_fold |
|
114 |
|
115 keyword1, keyword2 :: String -> T |
|
116 keyword1 name = mark_str (Markup.keyword1, name) |
|
117 keyword2 name = mark_str (Markup.keyword2, name) |
|
118 |
|
119 text :: String -> [T] |
|
120 text = breaks . map str . words |
|
121 |
|
122 paragraph :: [T] -> T |
|
123 paragraph = markup Markup.paragraph |
|
124 |
|
125 para :: String -> T |
|
126 para = paragraph . text |
|
127 |
|
128 quote :: T -> T |
|
129 quote prt = blk (1, [str "\"", prt, str "\""]) |
|
130 |
|
131 cartouche :: T -> T |
|
132 cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"]) |
|
133 |
|
134 separate :: String -> [T] -> [T] |
|
135 separate sep = List.intercalate [str sep, brk 1] . map single |
|
136 |
|
137 commas :: [T] -> [T] |
|
138 commas = separate "," |
|
139 |
|
140 enclose :: String -> String -> [T] -> T |
|
141 enclose lpar rpar prts = block (str lpar : prts ++ [str rpar]) |
|
142 |
|
143 enum :: String -> String -> String -> [T] -> T |
|
144 enum sep lpar rpar = enclose lpar rpar . separate sep |
|
145 |
|
146 list :: String -> String -> [T] -> T |
|
147 list = enum "," |
|
148 |
|
149 str_list :: String -> String -> [String] -> T |
|
150 str_list lpar rpar = list lpar rpar . map str |
|
151 |
|
152 big_list :: String -> [T] -> T |
|
153 big_list name prts = block (fbreaks (str name : prts)) |
|