244 module Isabelle.Markup ( |
247 module Isabelle.Markup ( |
245 T, empty, is_empty, properties, |
248 T, empty, is_empty, properties, |
246 |
249 |
247 nameN, name, xnameN, xname, kindN, |
250 nameN, name, xnameN, xname, kindN, |
248 |
251 |
|
252 completionN, completion, no_completionN, no_completion, |
|
253 |
249 lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position, |
254 lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position, |
250 |
255 |
251 markupN, consistentN, unbreakableN, indentN, widthN, |
256 markupN, consistentN, unbreakableN, indentN, widthN, |
252 blockN, block, breakN, break, fbreakN, fbreak, itemN, item, |
257 blockN, block, breakN, break, fbreakN, fbreak, itemN, item, |
253 |
258 |
522 |
536 |
523 type Output = (String, String) |
537 type Output = (String, String) |
524 |
538 |
525 no_output :: Output |
539 no_output :: Output |
526 no_output = ("", "") |
540 no_output = ("", "") |
|
541 \<close> |
|
542 |
|
543 generate_haskell_file "Completion.hs" = \<open> |
|
544 {- Title: Tools/Haskell/Completion.hs |
|
545 Author: Makarius |
|
546 LICENSE: BSD 3-clause (Isabelle) |
|
547 |
|
548 Completion of names. |
|
549 |
|
550 See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/completion.ML\<close>. |
|
551 -} |
|
552 |
|
553 module Isabelle.Completion (Name, T, names, none, make, encode, reported_text) |
|
554 where |
|
555 |
|
556 import qualified Data.List as List |
|
557 |
|
558 import Isabelle.Library |
|
559 import qualified Isabelle.Properties as Properties |
|
560 import qualified Isabelle.Markup as Markup |
|
561 import qualified Isabelle.XML.Encode as Encode |
|
562 import qualified Isabelle.XML as XML |
|
563 import qualified Isabelle.YXML as YXML |
|
564 |
|
565 |
|
566 type Name = (String, (String, String)) -- external name, kind, internal name |
|
567 data T = Completion Properties.T Int [Name] -- position, total length, names |
|
568 |
|
569 names :: Int -> Properties.T -> [Name] -> T |
|
570 names limit props names = Completion props (length names) (take limit names) |
|
571 |
|
572 none :: T |
|
573 none = names 0 [] [] |
|
574 |
|
575 make :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> T |
|
576 make limit (name, props) make_names = |
|
577 if name /= "" && name /= "_" |
|
578 then names limit props (make_names $ List.isPrefixOf $ clean_name name) |
|
579 else none |
|
580 |
|
581 encode :: T -> XML.Body |
|
582 encode (Completion _ total names) = |
|
583 Encode.pair Encode.int |
|
584 (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string))) |
|
585 (total, names) |
|
586 |
|
587 reported_text :: T -> String |
|
588 reported_text completion@(Completion props total names) = |
|
589 if not (null names) then |
|
590 let markup = Markup.properties props Markup.completion |
|
591 in YXML.string_of $ XML.Elem markup (encode completion) |
|
592 else "" |
527 \<close> |
593 \<close> |
528 |
594 |
529 generate_haskell_file "File.hs" = \<open> |
595 generate_haskell_file "File.hs" = \<open> |
530 {- Title: Tools/Haskell/File.hs |
596 {- Title: Tools/Haskell/File.hs |
531 Author: Makarius |
597 Author: Makarius |
835 variant fs [t] = (fs !! tag) (xs, ts) |
901 variant fs [t] = (fs !! tag) (xs, ts) |
836 where (tag, (xs, ts)) = tagged t |
902 where (tag, (xs, ts)) = tagged t |
837 variant _ _ = err_body |
903 variant _ _ = err_body |
838 \<close> |
904 \<close> |
839 |
905 |
840 generate_haskell_file "Pretty.hs" = \<open> |
|
841 {- Title: Tools/Haskell/Pretty.hs |
|
842 Author: Makarius |
|
843 LICENSE: BSD 3-clause (Isabelle) |
|
844 |
|
845 Generic pretty printing module. |
|
846 |
|
847 See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>. |
|
848 -} |
|
849 |
|
850 module Isabelle.Pretty ( |
|
851 T, symbolic, formatted, unformatted, |
|
852 |
|
853 str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str, |
|
854 item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate, |
|
855 commas, enclose, enum, list, str_list, big_list) |
|
856 where |
|
857 |
|
858 import Isabelle.Library hiding (quote) |
|
859 import qualified Data.List as List |
|
860 import qualified Isabelle.Buffer as Buffer |
|
861 import qualified Isabelle.Markup as Markup |
|
862 import qualified Isabelle.XML as XML |
|
863 import qualified Isabelle.YXML as YXML |
|
864 |
|
865 |
|
866 data T = |
|
867 Block Markup.T Bool Int [T] |
|
868 | Break Int Int |
|
869 | Str String |
|
870 |
|
871 |
|
872 {- output -} |
|
873 |
|
874 output_spaces n = replicate n ' ' |
|
875 |
|
876 symbolic_text "" = [] |
|
877 symbolic_text s = [XML.Text s] |
|
878 |
|
879 symbolic_markup markup body = |
|
880 if Markup.is_empty markup then body |
|
881 else [XML.Elem markup body] |
|
882 |
|
883 symbolic :: T -> XML.Body |
|
884 symbolic (Block markup consistent indent prts) = |
|
885 concatMap symbolic prts |
|
886 |> symbolic_markup block_markup |
|
887 |> symbolic_markup markup |
|
888 where block_markup = if null prts then Markup.empty else Markup.block consistent indent |
|
889 symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind) (symbolic_text (output_spaces wd))] |
|
890 symbolic (Str s) = symbolic_text s |
|
891 |
|
892 formatted :: T -> String |
|
893 formatted = YXML.string_of_body . symbolic |
|
894 |
|
895 unformatted :: T -> String |
|
896 unformatted prt = Buffer.empty |> out prt |> Buffer.content |
|
897 where |
|
898 out (Block markup _ _ prts) = |
|
899 let (bg, en) = YXML.output_markup markup |
|
900 in Buffer.add bg #> fold out prts #> Buffer.add en |
|
901 out (Break _ wd) = Buffer.add (output_spaces wd) |
|
902 out (Str s) = Buffer.add s |
|
903 |
|
904 |
|
905 {- derived operations to create formatting expressions -} |
|
906 |
|
907 force_nat n | n < 0 = 0 |
|
908 force_nat n = n |
|
909 |
|
910 str :: String -> T |
|
911 str = Str |
|
912 |
|
913 brk_indent :: Int -> Int -> T |
|
914 brk_indent wd ind = Break (force_nat wd) ind |
|
915 |
|
916 brk :: Int -> T |
|
917 brk wd = brk_indent wd 0 |
|
918 |
|
919 fbrk :: T |
|
920 fbrk = str "\n" |
|
921 |
|
922 breaks, fbreaks :: [T] -> [T] |
|
923 breaks = List.intersperse (brk 1) |
|
924 fbreaks = List.intersperse fbrk |
|
925 |
|
926 blk :: (Int, [T]) -> T |
|
927 blk (indent, es) = Block Markup.empty False (force_nat indent) es |
|
928 |
|
929 block :: [T] -> T |
|
930 block prts = blk (2, prts) |
|
931 |
|
932 strs :: [String] -> T |
|
933 strs = block . breaks . map str |
|
934 |
|
935 markup :: Markup.T -> [T] -> T |
|
936 markup m = Block m False 0 |
|
937 |
|
938 mark :: Markup.T -> T -> T |
|
939 mark m prt = if m == Markup.empty then prt else markup m [prt] |
|
940 |
|
941 mark_str :: (Markup.T, String) -> T |
|
942 mark_str (m, s) = mark m (str s) |
|
943 |
|
944 marks_str :: ([Markup.T], String) -> T |
|
945 marks_str (ms, s) = fold_rev mark ms (str s) |
|
946 |
|
947 item :: [T] -> T |
|
948 item = markup Markup.item |
|
949 |
|
950 text_fold :: [T] -> T |
|
951 text_fold = markup Markup.text_fold |
|
952 |
|
953 keyword1, keyword2 :: String -> T |
|
954 keyword1 name = mark_str (Markup.keyword1, name) |
|
955 keyword2 name = mark_str (Markup.keyword2, name) |
|
956 |
|
957 text :: String -> [T] |
|
958 text = breaks . map str . words |
|
959 |
|
960 paragraph :: [T] -> T |
|
961 paragraph = markup Markup.paragraph |
|
962 |
|
963 para :: String -> T |
|
964 para = paragraph . text |
|
965 |
|
966 quote :: T -> T |
|
967 quote prt = blk (1, [str "\"", prt, str "\""]) |
|
968 |
|
969 cartouche :: T -> T |
|
970 cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"]) |
|
971 |
|
972 separate :: String -> [T] -> [T] |
|
973 separate sep = List.intercalate [str sep, brk 1] . map single |
|
974 |
|
975 commas :: [T] -> [T] |
|
976 commas = separate "," |
|
977 |
|
978 enclose :: String -> String -> [T] -> T |
|
979 enclose lpar rpar prts = block (str lpar : prts ++ [str rpar]) |
|
980 |
|
981 enum :: String -> String -> String -> [T] -> T |
|
982 enum sep lpar rpar = enclose lpar rpar . separate sep |
|
983 |
|
984 list :: String -> String -> [T] -> T |
|
985 list = enum "," |
|
986 |
|
987 str_list :: String -> String -> [String] -> T |
|
988 str_list lpar rpar = list lpar rpar . map str |
|
989 |
|
990 big_list :: String -> [T] -> T |
|
991 big_list name prts = block (fbreaks (str name : prts)) |
|
992 \<close> |
|
993 |
|
994 generate_haskell_file "YXML.hs" = \<open> |
906 generate_haskell_file "YXML.hs" = \<open> |
995 {- Title: Tools/Haskell/YXML.hs |
907 {- Title: Tools/Haskell/YXML.hs |
996 Author: Makarius |
908 Author: Makarius |
997 LICENSE: BSD 3-clause (Isabelle) |
909 LICENSE: BSD 3-clause (Isabelle) |
998 |
910 |
1117 [result] -> result |
1029 [result] -> result |
1118 [] -> XML.Text "" |
1030 [] -> XML.Text "" |
1119 _ -> err "multiple results" |
1031 _ -> err "multiple results" |
1120 \<close> |
1032 \<close> |
1121 |
1033 |
|
1034 generate_haskell_file "Pretty.hs" = \<open> |
|
1035 {- Title: Tools/Haskell/Pretty.hs |
|
1036 Author: Makarius |
|
1037 LICENSE: BSD 3-clause (Isabelle) |
|
1038 |
|
1039 Generic pretty printing module. |
|
1040 |
|
1041 See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>. |
|
1042 -} |
|
1043 |
|
1044 module Isabelle.Pretty ( |
|
1045 T, symbolic, formatted, unformatted, |
|
1046 |
|
1047 str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str, |
|
1048 item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate, |
|
1049 commas, enclose, enum, list, str_list, big_list) |
|
1050 where |
|
1051 |
|
1052 import Isabelle.Library hiding (quote) |
|
1053 import qualified Data.List as List |
|
1054 import qualified Isabelle.Buffer as Buffer |
|
1055 import qualified Isabelle.Markup as Markup |
|
1056 import qualified Isabelle.XML as XML |
|
1057 import qualified Isabelle.YXML as YXML |
|
1058 |
|
1059 |
|
1060 data T = |
|
1061 Block Markup.T Bool Int [T] |
|
1062 | Break Int Int |
|
1063 | Str String |
|
1064 |
|
1065 |
|
1066 {- output -} |
|
1067 |
|
1068 output_spaces n = replicate n ' ' |
|
1069 |
|
1070 symbolic_text "" = [] |
|
1071 symbolic_text s = [XML.Text s] |
|
1072 |
|
1073 symbolic_markup markup body = |
|
1074 if Markup.is_empty markup then body |
|
1075 else [XML.Elem markup body] |
|
1076 |
|
1077 symbolic :: T -> XML.Body |
|
1078 symbolic (Block markup consistent indent prts) = |
|
1079 concatMap symbolic prts |
|
1080 |> symbolic_markup block_markup |
|
1081 |> symbolic_markup markup |
|
1082 where block_markup = if null prts then Markup.empty else Markup.block consistent indent |
|
1083 symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind) (symbolic_text (output_spaces wd))] |
|
1084 symbolic (Str s) = symbolic_text s |
|
1085 |
|
1086 formatted :: T -> String |
|
1087 formatted = YXML.string_of_body . symbolic |
|
1088 |
|
1089 unformatted :: T -> String |
|
1090 unformatted prt = Buffer.empty |> out prt |> Buffer.content |
|
1091 where |
|
1092 out (Block markup _ _ prts) = |
|
1093 let (bg, en) = YXML.output_markup markup |
|
1094 in Buffer.add bg #> fold out prts #> Buffer.add en |
|
1095 out (Break _ wd) = Buffer.add (output_spaces wd) |
|
1096 out (Str s) = Buffer.add s |
|
1097 |
|
1098 |
|
1099 {- derived operations to create formatting expressions -} |
|
1100 |
|
1101 force_nat n | n < 0 = 0 |
|
1102 force_nat n = n |
|
1103 |
|
1104 str :: String -> T |
|
1105 str = Str |
|
1106 |
|
1107 brk_indent :: Int -> Int -> T |
|
1108 brk_indent wd ind = Break (force_nat wd) ind |
|
1109 |
|
1110 brk :: Int -> T |
|
1111 brk wd = brk_indent wd 0 |
|
1112 |
|
1113 fbrk :: T |
|
1114 fbrk = str "\n" |
|
1115 |
|
1116 breaks, fbreaks :: [T] -> [T] |
|
1117 breaks = List.intersperse (brk 1) |
|
1118 fbreaks = List.intersperse fbrk |
|
1119 |
|
1120 blk :: (Int, [T]) -> T |
|
1121 blk (indent, es) = Block Markup.empty False (force_nat indent) es |
|
1122 |
|
1123 block :: [T] -> T |
|
1124 block prts = blk (2, prts) |
|
1125 |
|
1126 strs :: [String] -> T |
|
1127 strs = block . breaks . map str |
|
1128 |
|
1129 markup :: Markup.T -> [T] -> T |
|
1130 markup m = Block m False 0 |
|
1131 |
|
1132 mark :: Markup.T -> T -> T |
|
1133 mark m prt = if m == Markup.empty then prt else markup m [prt] |
|
1134 |
|
1135 mark_str :: (Markup.T, String) -> T |
|
1136 mark_str (m, s) = mark m (str s) |
|
1137 |
|
1138 marks_str :: ([Markup.T], String) -> T |
|
1139 marks_str (ms, s) = fold_rev mark ms (str s) |
|
1140 |
|
1141 item :: [T] -> T |
|
1142 item = markup Markup.item |
|
1143 |
|
1144 text_fold :: [T] -> T |
|
1145 text_fold = markup Markup.text_fold |
|
1146 |
|
1147 keyword1, keyword2 :: String -> T |
|
1148 keyword1 name = mark_str (Markup.keyword1, name) |
|
1149 keyword2 name = mark_str (Markup.keyword2, name) |
|
1150 |
|
1151 text :: String -> [T] |
|
1152 text = breaks . map str . words |
|
1153 |
|
1154 paragraph :: [T] -> T |
|
1155 paragraph = markup Markup.paragraph |
|
1156 |
|
1157 para :: String -> T |
|
1158 para = paragraph . text |
|
1159 |
|
1160 quote :: T -> T |
|
1161 quote prt = blk (1, [str "\"", prt, str "\""]) |
|
1162 |
|
1163 cartouche :: T -> T |
|
1164 cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"]) |
|
1165 |
|
1166 separate :: String -> [T] -> [T] |
|
1167 separate sep = List.intercalate [str sep, brk 1] . map single |
|
1168 |
|
1169 commas :: [T] -> [T] |
|
1170 commas = separate "," |
|
1171 |
|
1172 enclose :: String -> String -> [T] -> T |
|
1173 enclose lpar rpar prts = block (str lpar : prts ++ [str rpar]) |
|
1174 |
|
1175 enum :: String -> String -> String -> [T] -> T |
|
1176 enum sep lpar rpar = enclose lpar rpar . separate sep |
|
1177 |
|
1178 list :: String -> String -> [T] -> T |
|
1179 list = enum "," |
|
1180 |
|
1181 str_list :: String -> String -> [String] -> T |
|
1182 str_list lpar rpar = list lpar rpar . map str |
|
1183 |
|
1184 big_list :: String -> [T] -> T |
|
1185 big_list name prts = block (fbreaks (str name : prts)) |
|
1186 \<close> |
|
1187 |
1122 generate_haskell_file "Term.hs" = \<open> |
1188 generate_haskell_file "Term.hs" = \<open> |
1123 {- Title: Tools/Haskell/Term.hs |
1189 {- Title: Tools/Haskell/Term.hs |
1124 Author: Makarius |
1190 Author: Makarius |
1125 LICENSE: BSD 3-clause (Isabelle) |
1191 LICENSE: BSD 3-clause (Isabelle) |
1126 |
1192 |