merged
authorwenzelm
Tue Nov 06 15:06:30 2018 +0100 (7 months ago)
changeset 6924927423819534c
parent 69246 c1fe9dcc274a
parent 69248 9f21381600e3
child 69250 1011f0b46af7
child 69253 8bfa615ddde4
merged
     1.1 --- a/src/Pure/General/pretty.ML	Sun Nov 04 15:00:30 2018 +0000
     1.2 +++ b/src/Pure/General/pretty.ML	Tue Nov 06 15:06:30 2018 +0100
     1.3 @@ -326,10 +326,10 @@
     1.4  (*unformatted output*)
     1.5  fun unformatted prt =
     1.6    let
     1.7 -    fun fmt (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
     1.8 -      | fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd)
     1.9 -      | fmt (Str (s, _)) = Buffer.add s;
    1.10 -  in fmt prt Buffer.empty end;
    1.11 +    fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
    1.12 +      | out (Break (_, wd, _)) = Buffer.add (output_spaces wd)
    1.13 +      | out (Str (s, _)) = Buffer.add s;
    1.14 +  in out prt Buffer.empty end;
    1.15  
    1.16  
    1.17  (* output interfaces *)
     2.1 --- a/src/Tools/Haskell/Haskell.thy	Sun Nov 04 15:00:30 2018 +0000
     2.2 +++ b/src/Tools/Haskell/Haskell.thy	Tue Nov 06 15:06:30 2018 +0100
     2.3 @@ -238,6 +238,9 @@
     2.4  
     2.5    lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
     2.6  
     2.7 +  markupN, consistentN, unbreakableN, indentN, widthN,
     2.8 +  blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
     2.9 +
    2.10    wordsN, words, no_wordsN, no_words,
    2.11  
    2.12    tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
    2.13 @@ -261,10 +264,11 @@
    2.14    Output, no_output)
    2.15  where
    2.16  
    2.17 -import Prelude hiding (words, error)
    2.18 +import Prelude hiding (words, error, break)
    2.19  
    2.20  import Isabelle.Library
    2.21  import qualified Isabelle.Properties as Properties
    2.22 +import qualified Isabelle.Value as Value
    2.23  
    2.24  
    2.25  {- basic markup -}
    2.26 @@ -321,6 +325,40 @@
    2.27  (positionN, position) = markup_elem \<open>Markup.positionN\<close>
    2.28  
    2.29  
    2.30 +{- pretty printing -}
    2.31 +
    2.32 +markupN, consistentN, unbreakableN, indentN :: String
    2.33 +markupN = \<open>Markup.markupN\<close>;
    2.34 +consistentN = \<open>Markup.consistentN\<close>;
    2.35 +unbreakableN = \<open>Markup.unbreakableN\<close>;
    2.36 +indentN = \<open>Markup.indentN\<close>;
    2.37 +
    2.38 +widthN :: String
    2.39 +widthN = \<open>Markup.widthN\<close>
    2.40 +
    2.41 +blockN :: String
    2.42 +blockN = \<open>Markup.blockN\<close>
    2.43 +block :: Bool -> Int -> T
    2.44 +block c i =
    2.45 +  (blockN,
    2.46 +    (if c then [(consistentN, Value.print_bool c)] else []) ++
    2.47 +    (if i /= 0 then [(indentN, Value.print_int i)] else []))
    2.48 +
    2.49 +breakN :: String
    2.50 +breakN = \<open>Markup.breakN\<close>
    2.51 +break :: Int -> Int -> T
    2.52 +break w i =
    2.53 +  (breakN,
    2.54 +    (if w /= 0 then [(widthN, Value.print_int w)] else []) ++
    2.55 +    (if i /= 0 then [(indentN, Value.print_int i)] else []))
    2.56 +
    2.57 +fbreakN :: String; fbreak :: T
    2.58 +(fbreakN, fbreak) = markup_elem \<open>Markup.fbreakN\<close>
    2.59 +
    2.60 +itemN :: String; item :: T
    2.61 +(itemN, item) = markup_elem \<open>Markup.itemN\<close>
    2.62 +
    2.63 +
    2.64  {- text properties -}
    2.65  
    2.66  wordsN :: String; words :: T
    2.67 @@ -748,6 +786,158 @@
    2.68  variant _ _ = err_body
    2.69  \<close>
    2.70  
    2.71 +generate_haskell_file "Pretty.hs" = \<open>
    2.72 +{-  Title:      Tools/Haskell/Pretty.hs
    2.73 +    Author:     Makarius
    2.74 +    LICENSE:    BSD 3-clause (Isabelle)
    2.75 +
    2.76 +Generic pretty printing module.
    2.77 +-}
    2.78 +
    2.79 +module Isabelle.Pretty (
    2.80 +  T, symbolic, formatted, unformatted,
    2.81 +
    2.82 +  str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
    2.83 +  item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
    2.84 +  commas, enclose, enum, list, str_list, big_list)
    2.85 +where
    2.86 +
    2.87 +import Isabelle.Library hiding (quote)
    2.88 +import qualified Data.List as List
    2.89 +import qualified Isabelle.Buffer as Buffer
    2.90 +import qualified Isabelle.Markup as Markup
    2.91 +import qualified Isabelle.XML as XML
    2.92 +import qualified Isabelle.YXML as YXML
    2.93 +
    2.94 +
    2.95 +data T =
    2.96 +    Block Markup.T Bool Int [T]
    2.97 +  | Break Int Int
    2.98 +  | Str String
    2.99 +
   2.100 +
   2.101 +{- output -}
   2.102 +
   2.103 +output_spaces n = replicate n ' '
   2.104 +
   2.105 +symbolic_text "" = []
   2.106 +symbolic_text s = [XML.Text s]
   2.107 +
   2.108 +symbolic_markup markup body =
   2.109 +  if Markup.is_empty markup then body
   2.110 +  else [XML.Elem markup body]
   2.111 +
   2.112 +symbolic :: T -> XML.Body
   2.113 +symbolic (Block markup consistent indent prts) =
   2.114 +  concatMap symbolic prts
   2.115 +  |> symbolic_markup block_markup
   2.116 +  |> symbolic_markup markup
   2.117 +  where block_markup = if null prts then Markup.empty else Markup.block consistent indent
   2.118 +symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind) (symbolic_text (output_spaces wd))]
   2.119 +symbolic (Str s) = symbolic_text s
   2.120 +
   2.121 +formatted :: T -> String
   2.122 +formatted = YXML.string_of_body . symbolic
   2.123 +
   2.124 +unformatted :: T -> String
   2.125 +unformatted prt = Buffer.empty |> out prt |> Buffer.content
   2.126 +  where
   2.127 +    out (Block markup _ _ prts) =
   2.128 +      let (bg, en) = YXML.output_markup markup
   2.129 +      in Buffer.add bg #> fold out prts #> Buffer.add en
   2.130 +    out (Break _ wd) = Buffer.add (output_spaces wd)
   2.131 +    out (Str s) = Buffer.add s
   2.132 +
   2.133 +
   2.134 +{- derived operations to create formatting expressions -}
   2.135 +
   2.136 +force_nat n | n < 0 = 0
   2.137 +force_nat n = n
   2.138 +
   2.139 +str :: String -> T
   2.140 +str = Str
   2.141 +
   2.142 +brk_indent :: Int -> Int -> T
   2.143 +brk_indent wd ind = Break (force_nat wd) ind
   2.144 +
   2.145 +brk :: Int -> T
   2.146 +brk wd = brk_indent wd 0
   2.147 +
   2.148 +fbrk :: T
   2.149 +fbrk = str "\n"
   2.150 +
   2.151 +breaks, fbreaks :: [T] -> [T]
   2.152 +breaks = List.intersperse (brk 1)
   2.153 +fbreaks = List.intersperse fbrk
   2.154 +
   2.155 +blk :: (Int, [T]) -> T
   2.156 +blk (indent, es) = Block Markup.empty False (force_nat indent) es
   2.157 +
   2.158 +block :: [T] -> T
   2.159 +block prts = blk (2, prts)
   2.160 +
   2.161 +strs :: [String] -> T
   2.162 +strs = block . breaks . map str
   2.163 +
   2.164 +markup :: Markup.T -> [T] -> T
   2.165 +markup m = Block m False 0
   2.166 +
   2.167 +mark :: Markup.T -> T -> T
   2.168 +mark m prt = if m == Markup.empty then prt else markup m [prt]
   2.169 +
   2.170 +mark_str :: (Markup.T, String) -> T
   2.171 +mark_str (m, s) = mark m (str s)
   2.172 +
   2.173 +marks_str :: ([Markup.T], String) -> T
   2.174 +marks_str (ms, s) = fold_rev mark ms (str s)
   2.175 +
   2.176 +item :: [T] -> T
   2.177 +item = markup Markup.item
   2.178 +
   2.179 +text_fold :: [T] -> T
   2.180 +text_fold = markup Markup.text_fold
   2.181 +
   2.182 +keyword1, keyword2 :: String -> T
   2.183 +keyword1 name = mark_str (Markup.keyword1, name)
   2.184 +keyword2 name = mark_str (Markup.keyword2, name)
   2.185 +
   2.186 +text :: String -> [T]
   2.187 +text = breaks . map str . words
   2.188 +
   2.189 +paragraph :: [T] -> T
   2.190 +paragraph = markup Markup.paragraph
   2.191 +
   2.192 +para :: String -> T
   2.193 +para = paragraph . text
   2.194 +
   2.195 +quote :: T -> T
   2.196 +quote prt = blk (1, [str "\"", prt, str "\""])
   2.197 +
   2.198 +cartouche :: T -> T
   2.199 +cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"])
   2.200 +
   2.201 +separate :: String -> [T] -> [T]
   2.202 +separate sep = List.intercalate [str sep, brk 1] . map single
   2.203 +
   2.204 +commas :: [T] -> [T]
   2.205 +commas = separate ","
   2.206 +
   2.207 +enclose :: String -> String -> [T] -> T
   2.208 +enclose lpar rpar prts = block (str lpar : prts ++ [str rpar])
   2.209 +
   2.210 +enum :: String -> String -> String -> [T] -> T
   2.211 +enum sep lpar rpar = enclose lpar rpar . separate sep
   2.212 +
   2.213 +list :: String -> String -> [T] -> T
   2.214 +list = enum ","
   2.215 +
   2.216 +str_list :: String -> String -> [String] -> T
   2.217 +str_list lpar rpar = list lpar rpar . map str
   2.218 +
   2.219 +big_list :: String -> [T] -> T
   2.220 +big_list name prts = block (fbreaks (str name : prts))
   2.221 +\<close>
   2.222 +
   2.223  generate_haskell_file "YXML.hs" = \<open>
   2.224  {-  Title:      Tools/Haskell/YXML.hs
   2.225      Author:     Makarius
   2.226 @@ -757,7 +947,7 @@
   2.227  inlining into plain text.
   2.228  -}
   2.229  
   2.230 -module Isabelle.YXML (charX, charY, strX, strY, detect,
   2.231 +module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
   2.232    buffer_body, buffer, string_of_body, string_of, parse_body, parse)
   2.233  where
   2.234  
   2.235 @@ -788,6 +978,11 @@
   2.236  
   2.237  {- output -}
   2.238  
   2.239 +output_markup :: Markup.T -> Markup.Output
   2.240 +output_markup markup@(name, atts) =
   2.241 +  if Markup.is_empty markup then Markup.no_output
   2.242 +  else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX)
   2.243 +
   2.244  buffer_attrib (a, x) =
   2.245    Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
   2.246  
     3.1 --- a/src/Tools/Haskell/Markup.hs	Sun Nov 04 15:00:30 2018 +0000
     3.2 +++ b/src/Tools/Haskell/Markup.hs	Tue Nov 06 15:06:30 2018 +0100
     3.3 @@ -14,6 +14,9 @@
     3.4  
     3.5    lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
     3.6  
     3.7 +  markupN, consistentN, unbreakableN, indentN, widthN,
     3.8 +  blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
     3.9 +
    3.10    wordsN, words, no_wordsN, no_words,
    3.11  
    3.12    tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
    3.13 @@ -37,10 +40,11 @@
    3.14    Output, no_output)
    3.15  where
    3.16  
    3.17 -import Prelude hiding (words, error)
    3.18 +import Prelude hiding (words, error, break)
    3.19  
    3.20  import Isabelle.Library
    3.21  import qualified Isabelle.Properties as Properties
    3.22 +import qualified Isabelle.Value as Value
    3.23  
    3.24  
    3.25  {- basic markup -}
    3.26 @@ -97,6 +101,40 @@
    3.27  (positionN, position) = markup_elem "position"
    3.28  
    3.29  
    3.30 +{- pretty printing -}
    3.31 +
    3.32 +markupN, consistentN, unbreakableN, indentN :: String
    3.33 +markupN = "markup";
    3.34 +consistentN = "consistent";
    3.35 +unbreakableN = "unbreakable";
    3.36 +indentN = "indent";
    3.37 +
    3.38 +widthN :: String
    3.39 +widthN = "width"
    3.40 +
    3.41 +blockN :: String
    3.42 +blockN = "block"
    3.43 +block :: Bool -> Int -> T
    3.44 +block c i =
    3.45 +  (blockN,
    3.46 +    (if c then [(consistentN, Value.print_bool c)] else []) ++
    3.47 +    (if i /= 0 then [(indentN, Value.print_int i)] else []))
    3.48 +
    3.49 +breakN :: String
    3.50 +breakN = "break"
    3.51 +break :: Int -> Int -> T
    3.52 +break w i =
    3.53 +  (breakN,
    3.54 +    (if w /= 0 then [(widthN, Value.print_int w)] else []) ++
    3.55 +    (if i /= 0 then [(indentN, Value.print_int i)] else []))
    3.56 +
    3.57 +fbreakN :: String; fbreak :: T
    3.58 +(fbreakN, fbreak) = markup_elem "fbreak"
    3.59 +
    3.60 +itemN :: String; item :: T
    3.61 +(itemN, item) = markup_elem "item"
    3.62 +
    3.63 +
    3.64  {- text properties -}
    3.65  
    3.66  wordsN :: String; words :: T
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/Haskell/Pretty.hs	Tue Nov 06 15:06:30 2018 +0100
     4.3 @@ -0,0 +1,151 @@
     4.4 +{- generated by Isabelle -}
     4.5 +
     4.6 +{-  Title:      Tools/Haskell/Pretty.hs
     4.7 +    Author:     Makarius
     4.8 +    LICENSE:    BSD 3-clause (Isabelle)
     4.9 +
    4.10 +Generic pretty printing module.
    4.11 +-}
    4.12 +
    4.13 +module Isabelle.Pretty (
    4.14 +  T, symbolic, formatted, unformatted,
    4.15 +
    4.16 +  str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
    4.17 +  item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
    4.18 +  commas, enclose, enum, list, str_list, big_list)
    4.19 +where
    4.20 +
    4.21 +import Isabelle.Library hiding (quote)
    4.22 +import qualified Data.List as List
    4.23 +import qualified Isabelle.Buffer as Buffer
    4.24 +import qualified Isabelle.Markup as Markup
    4.25 +import qualified Isabelle.XML as XML
    4.26 +import qualified Isabelle.YXML as YXML
    4.27 +
    4.28 +
    4.29 +data T =
    4.30 +    Block Markup.T Bool Int [T]
    4.31 +  | Break Int Int
    4.32 +  | Str String
    4.33 +
    4.34 +
    4.35 +{- output -}
    4.36 +
    4.37 +output_spaces n = replicate n ' '
    4.38 +
    4.39 +symbolic_text "" = []
    4.40 +symbolic_text s = [XML.Text s]
    4.41 +
    4.42 +symbolic_markup markup body =
    4.43 +  if Markup.is_empty markup then body
    4.44 +  else [XML.Elem markup body]
    4.45 +
    4.46 +symbolic :: T -> XML.Body
    4.47 +symbolic (Block markup consistent indent prts) =
    4.48 +  concatMap symbolic prts
    4.49 +  |> symbolic_markup block_markup
    4.50 +  |> symbolic_markup markup
    4.51 +  where block_markup = if null prts then Markup.empty else Markup.block consistent indent
    4.52 +symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind) (symbolic_text (output_spaces wd))]
    4.53 +symbolic (Str s) = symbolic_text s
    4.54 +
    4.55 +formatted :: T -> String
    4.56 +formatted = YXML.string_of_body . symbolic
    4.57 +
    4.58 +unformatted :: T -> String
    4.59 +unformatted prt = Buffer.empty |> out prt |> Buffer.content
    4.60 +  where
    4.61 +    out (Block markup _ _ prts) =
    4.62 +      let (bg, en) = YXML.output_markup markup
    4.63 +      in Buffer.add bg #> fold out prts #> Buffer.add en
    4.64 +    out (Break _ wd) = Buffer.add (output_spaces wd)
    4.65 +    out (Str s) = Buffer.add s
    4.66 +
    4.67 +
    4.68 +{- derived operations to create formatting expressions -}
    4.69 +
    4.70 +force_nat n | n < 0 = 0
    4.71 +force_nat n = n
    4.72 +
    4.73 +str :: String -> T
    4.74 +str = Str
    4.75 +
    4.76 +brk_indent :: Int -> Int -> T
    4.77 +brk_indent wd ind = Break (force_nat wd) ind
    4.78 +
    4.79 +brk :: Int -> T
    4.80 +brk wd = brk_indent wd 0
    4.81 +
    4.82 +fbrk :: T
    4.83 +fbrk = str "\n"
    4.84 +
    4.85 +breaks, fbreaks :: [T] -> [T]
    4.86 +breaks = List.intersperse (brk 1)
    4.87 +fbreaks = List.intersperse fbrk
    4.88 +
    4.89 +blk :: (Int, [T]) -> T
    4.90 +blk (indent, es) = Block Markup.empty False (force_nat indent) es
    4.91 +
    4.92 +block :: [T] -> T
    4.93 +block prts = blk (2, prts)
    4.94 +
    4.95 +strs :: [String] -> T
    4.96 +strs = block . breaks . map str
    4.97 +
    4.98 +markup :: Markup.T -> [T] -> T
    4.99 +markup m = Block m False 0
   4.100 +
   4.101 +mark :: Markup.T -> T -> T
   4.102 +mark m prt = if m == Markup.empty then prt else markup m [prt]
   4.103 +
   4.104 +mark_str :: (Markup.T, String) -> T
   4.105 +mark_str (m, s) = mark m (str s)
   4.106 +
   4.107 +marks_str :: ([Markup.T], String) -> T
   4.108 +marks_str (ms, s) = fold_rev mark ms (str s)
   4.109 +
   4.110 +item :: [T] -> T
   4.111 +item = markup Markup.item
   4.112 +
   4.113 +text_fold :: [T] -> T
   4.114 +text_fold = markup Markup.text_fold
   4.115 +
   4.116 +keyword1, keyword2 :: String -> T
   4.117 +keyword1 name = mark_str (Markup.keyword1, name)
   4.118 +keyword2 name = mark_str (Markup.keyword2, name)
   4.119 +
   4.120 +text :: String -> [T]
   4.121 +text = breaks . map str . words
   4.122 +
   4.123 +paragraph :: [T] -> T
   4.124 +paragraph = markup Markup.paragraph
   4.125 +
   4.126 +para :: String -> T
   4.127 +para = paragraph . text
   4.128 +
   4.129 +quote :: T -> T
   4.130 +quote prt = blk (1, [str "\"", prt, str "\""])
   4.131 +
   4.132 +cartouche :: T -> T
   4.133 +cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"])
   4.134 +
   4.135 +separate :: String -> [T] -> [T]
   4.136 +separate sep = List.intercalate [str sep, brk 1] . map single
   4.137 +
   4.138 +commas :: [T] -> [T]
   4.139 +commas = separate ","
   4.140 +
   4.141 +enclose :: String -> String -> [T] -> T
   4.142 +enclose lpar rpar prts = block (str lpar : prts ++ [str rpar])
   4.143 +
   4.144 +enum :: String -> String -> String -> [T] -> T
   4.145 +enum sep lpar rpar = enclose lpar rpar . separate sep
   4.146 +
   4.147 +list :: String -> String -> [T] -> T
   4.148 +list = enum ","
   4.149 +
   4.150 +str_list :: String -> String -> [String] -> T
   4.151 +str_list lpar rpar = list lpar rpar . map str
   4.152 +
   4.153 +big_list :: String -> [T] -> T
   4.154 +big_list name prts = block (fbreaks (str name : prts))
     5.1 --- a/src/Tools/Haskell/YXML.hs	Sun Nov 04 15:00:30 2018 +0000
     5.2 +++ b/src/Tools/Haskell/YXML.hs	Tue Nov 06 15:06:30 2018 +0100
     5.3 @@ -8,7 +8,7 @@
     5.4  inlining into plain text.
     5.5  -}
     5.6  
     5.7 -module Isabelle.YXML (charX, charY, strX, strY, detect,
     5.8 +module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
     5.9    buffer_body, buffer, string_of_body, string_of, parse_body, parse)
    5.10  where
    5.11  
    5.12 @@ -39,6 +39,11 @@
    5.13  
    5.14  {- output -}
    5.15  
    5.16 +output_markup :: Markup.T -> Markup.Output
    5.17 +output_markup markup@(name, atts) =
    5.18 +  if Markup.is_empty markup then Markup.no_output
    5.19 +  else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX)
    5.20 +
    5.21  buffer_attrib (a, x) =
    5.22    Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
    5.23  
     6.1 --- a/src/Tools/Haskell/haskell.ML	Sun Nov 04 15:00:30 2018 +0000
     6.2 +++ b/src/Tools/Haskell/haskell.ML	Tue Nov 06 15:06:30 2018 +0100
     6.3 @@ -56,6 +56,7 @@
     6.4    \<^path>\<open>XML/Encode.hs\<close>,
     6.5    \<^path>\<open>XML/Decode.hs\<close>,
     6.6    \<^path>\<open>YXML.hs\<close>,
     6.7 +  \<^path>\<open>Pretty.hs\<close>,
     6.8    \<^path>\<open>Term.hs\<close>,
     6.9    \<^path>\<open>Term_XML/Encode.hs\<close>,
    6.10    \<^path>\<open>Term_XML/Decode.hs\<close>];