changeset 336 | a12bb28fe2bd |
parent 335 | 163ac0662211 |
child 337 | a456a21f608a |
335:163ac0662211 | 336:a12bb28fe2bd |
---|---|
1129 local_setup %gray {* |
1129 local_setup %gray {* |
1130 LocalTheory.note Thm.theoremK |
1130 LocalTheory.note Thm.theoremK |
1131 ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *} |
1131 ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *} |
1132 |
1132 |
1133 |
1133 |
1134 (* FIXME: some code below *) |
|
1135 |
|
1136 (*<*) |
|
1137 (* |
1134 (* |
1138 setup {* |
1135 setup {* |
1139 Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] |
1136 Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] |
1140 *} |
1137 *} |
1141 *) |
|
1142 lemma "bar = (1::nat)" |
1138 lemma "bar = (1::nat)" |
1143 oops |
1139 oops |
1144 |
1140 |
1145 (* |
|
1146 setup {* |
1141 setup {* |
1147 Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] |
1142 Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] |
1148 #> PureThy.add_defs false [((@{binding "foo_def"}, |
1143 #> PureThy.add_defs false [((@{binding "foo_def"}, |
1149 Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] |
1144 Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] |
1150 #> snd |
1145 #> snd |
1155 apply(simp add: foo_def) |
1150 apply(simp add: foo_def) |
1156 done |
1151 done |
1157 |
1152 |
1158 thm foo_def |
1153 thm foo_def |
1159 *) |
1154 *) |
1160 (*>*) |
1155 |
1161 |
1156 |
1162 section {* Pretty-Printing\label{sec:pretty} *} |
1157 section {* Pretty-Printing\label{sec:pretty} *} |
1163 |
1158 |
1164 text {* |
1159 text {* |
1165 So far we printed out only plain strings without any formatting except for |
1160 So far we printed out only plain strings without any formatting except for |
1166 occasional explicit line breaks using @{text [quotes] "\\n"}. This is |
1161 occasional explicit line breaks using @{text [quotes] "\\n"}. This is |
1167 sufficient for ``quick-and-dirty'' printouts. For something more |
1162 sufficient for ``quick-and-dirty'' printouts. For something more |
1168 sophisticated, Isabelle includes an infrastructure for properly formatting text. |
1163 sophisticated, Isabelle includes an infrastructure for properly formatting |
1169 This infrastructure is loosely based on a paper by Oppen~\cite{Oppen80}. Most of |
1164 text. Most of its functions do not operate on @{ML_type string}s, but on |
1170 its functions do not operate on @{ML_type string}s, but on instances of the |
1165 instances of the pretty type: |
1171 type: |
|
1172 |
1166 |
1173 @{ML_type_ind [display, gray] "Pretty.T"} |
1167 @{ML_type_ind [display, gray] "Pretty.T"} |
1174 |
1168 |
1175 The function @{ML str in Pretty} transforms a (plain) string into such a pretty |
1169 The function @{ML str in Pretty} transforms a (plain) string into such a pretty |
1176 type. For example |
1170 type. For example |
1215 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo |
1209 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo |
1216 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa |
1210 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa |
1217 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo |
1211 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo |
1218 oooooooooooooobaaaaaaaaaaaar"} |
1212 oooooooooooooobaaaaaaaaaaaar"} |
1219 |
1213 |
1220 We obtain the same if we just use |
1214 We obtain the same if we just use the function @{ML pprint}. |
1221 |
1215 |
1222 @{ML_response_fake [display,gray] |
1216 @{ML_response_fake [display,gray] |
1223 "pprint (Pretty.str test_str)" |
1217 "pprint (Pretty.str test_str)" |
1224 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo |
1218 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo |
1225 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa |
1219 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa |
1226 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo |
1220 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo |
1227 oooooooooooooobaaaaaaaaaaaar"} |
1221 oooooooooooooobaaaaaaaaaaaar"} |
1228 |
1222 |
1229 However by using pretty types you have the ability to indicate a possible |
1223 However by using pretty types you have the ability to indicate possible |
1230 line break for example at each space. You can achieve this with the function |
1224 linebreaks for example at each whitespace. You can achieve this with the |
1231 @{ML_ind breaks in Pretty}, which expects a list of pretty types and inserts a |
1225 function @{ML_ind breaks in Pretty}, which expects a list of pretty types |
1232 possible line break in between every two elements in this list. To print |
1226 and inserts a possible line break in between every two elements in this |
1233 this list of pretty types as a single string, we concatenate them |
1227 list. To print this list of pretty types as a single string, we concatenate |
1234 with the function @{ML_ind blk in Pretty} as follows: |
1228 them with the function @{ML_ind blk in Pretty} as follows: |
1235 |
|
1236 |
1229 |
1237 @{ML_response_fake [display,gray] |
1230 @{ML_response_fake [display,gray] |
1238 "let |
1231 "let |
1239 val ptrs = map Pretty.str (space_explode \" \" test_str) |
1232 val ptrs = map Pretty.str (space_explode \" \" test_str) |
1240 in |
1233 in |
1306 "{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, |
1299 "{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, |
1307 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, |
1300 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, |
1308 100016, 100017, 100018, 100019, 100020}"} |
1301 100016, 100017, 100018, 100019, 100020}"} |
1309 |
1302 |
1310 As can be seen, this function prints out the ``set'' so that starting |
1303 As can be seen, this function prints out the ``set'' so that starting |
1311 from the second, each new line as an indentation of 2. |
1304 from the second, each new line has an indentation of 2. |
1312 |
1305 |
1313 If you print out something that goes beyond the capabilities of the |
1306 If you print out something that goes beyond the capabilities of the |
1314 standard functions, you can do relatively easily the formatting |
1307 standard functions, you can do relatively easily the formatting |
1315 yourself. Assume you want to print out a list of items where like in ``English'' |
1308 yourself. Assume you want to print out a list of items where like in ``English'' |
1316 the last two items are separated by @{text [quotes] "and"}. For this you can |
1309 the last two items are separated by @{text [quotes] "and"}. For this you can |
1336 can occur. We do the same after the @{text [quotes] "and"}. This gives you |
1329 can occur. We do the same after the @{text [quotes] "and"}. This gives you |
1337 for example |
1330 for example |
1338 |
1331 |
1339 @{ML_response_fake [display,gray] |
1332 @{ML_response_fake [display,gray] |
1340 "let |
1333 "let |
1341 val ptrs = map (Pretty.str o string_of_int) (1 upto 22) |
1334 val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22) |
1342 in |
1335 val ptrs2 = map (Pretty.str o string_of_int) (10 upto 28) |
1343 pprint (Pretty.blk (0, and_list ptrs)) |
1336 in |
1337 pprint (Pretty.blk (0, and_list ptrs1)); |
|
1338 pprint (Pretty.blk (0, and_list ptrs2)) |
|
1344 end" |
1339 end" |
1345 "1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 |
1340 "1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 |
1346 and 22"} |
1341 and 22 |
1342 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and |
|
1343 28"} |
|
1347 |
1344 |
1348 Next we like to pretty-print a term and its type. For this we use the |
1345 Next we like to pretty-print a term and its type. For this we use the |
1349 function @{text "tell_type"}. |
1346 function @{text "tell_type"}. |
1350 *} |
1347 *} |
1351 |
1348 |
1366 using the functions @{ML_ind pretty_term in Syntax} and @{ML_ind |
1363 using the functions @{ML_ind pretty_term in Syntax} and @{ML_ind |
1367 pretty_typ in Syntax}. We also use the function @{ML_ind quote in |
1364 pretty_typ in Syntax}. We also use the function @{ML_ind quote in |
1368 Pretty} in order to enclose the term and type inside quotation marks. In |
1365 Pretty} in order to enclose the term and type inside quotation marks. In |
1369 Line 9 we add a period right after the type without the possibility of a |
1366 Line 9 we add a period right after the type without the possibility of a |
1370 line break, because we do not want that a line break occurs there. |
1367 line break, because we do not want that a line break occurs there. |
1371 |
|
1372 |
|
1373 Now you can write |
1368 Now you can write |
1374 |
1369 |
1375 @{ML_response_fake [display,gray] |
1370 @{ML_response_fake [display,gray] |
1376 "tell_type @{context} @{term \"min (Suc 0)\"}" |
1371 "tell_type @{context} @{term \"min (Suc 0)\"}" |
1377 "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."} |
1372 "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."} |
1382 @{ML_response_fake [display,gray] |
1377 @{ML_response_fake [display,gray] |
1383 "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}" |
1378 "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}" |
1384 "The term \"op = (op = (op = (op = (op = op =))))\" has type |
1379 "The term \"op = (op = (op = (op = (op = op =))))\" has type |
1385 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."} |
1380 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."} |
1386 |
1381 |
1387 |
1382 The function @{ML_ind big_list in Pretty} helps with printing long lists. |
1388 FIXME: TBD below |
1383 It is used for example in the command \isacommand{print\_theorems}. An |
1389 *} |
1384 example is as follows. |
1390 |
1385 |
1391 ML {* pprint (Pretty.big_list "header" (map (Pretty.str o string_of_int) (4 upto 10))) *} |
1386 @{ML_response_fake [display,gray] |
1392 |
1387 "let |
1393 text {* |
1388 val pstrs = map (Pretty.str o string_of_int) (4 upto 10) |
1394 chunks inserts forced breaks (unlike blk where you have to do this yourself) |
1389 in |
1395 *} |
1390 pprint (Pretty.big_list \"header\" pstrs) |
1396 |
1391 end" |
1397 ML {* (Pretty.chunks [Pretty.str "a", Pretty.str "b"], |
1392 "header |
1398 Pretty.blk (0, [Pretty.str "a", Pretty.str "b"])) *} |
1393 4 |
1399 |
1394 5 |
1395 6 |
|
1396 7 |
|
1397 8 |
|
1398 9 |
|
1399 10"} |
|
1400 |
|
1401 Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out |
|
1402 a list of items, but automatically inserts forced breaks between each item. |
|
1403 Compare |
|
1404 |
|
1405 @{ML_response_fake [display,gray] |
|
1406 "let |
|
1407 val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"] |
|
1408 in |
|
1409 pprint (Pretty.blk (0, a_and_b)); |
|
1410 pprint (Pretty.chunks a_and_b) |
|
1411 end" |
|
1412 "ab |
|
1413 a |
|
1414 b"} |
|
1415 |
|
1416 \footnote{\bf What happens with printing big formulae?} |
|
1417 |
|
1418 |
|
1419 |
|
1420 \begin{readmore} |
|
1421 The general infrastructure for pretty-printing is implemented in the file |
|
1422 @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"} |
|
1423 contains pretty-printing functions for terms, types, theorems and so on. |
|
1424 |
|
1425 @{ML_file "Pure/General/markup.ML"} |
|
1426 \end{readmore} |
|
1427 *} |
|
1428 |
|
1429 (* |
|
1430 text {* |
|
1431 printing into the goal buffer as part of the proof state |
|
1432 *} |
|
1433 |
|
1434 text {* writing into the goal buffer *} |
|
1435 |
|
1436 ML {* fun my_hook interactive state = |
|
1437 (interactive ? Proof.goal_message (fn () => Pretty.str |
|
1438 "foo")) state |
|
1439 *} |
|
1440 |
|
1441 setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *} |
|
1442 |
|
1443 lemma "False" |
|
1444 oops |
|
1445 *) |
|
1446 |
|
1447 (* |
|
1400 ML {* |
1448 ML {* |
1401 fun setmp_show_all_types f = |
1449 fun setmp_show_all_types f = |
1402 setmp show_all_types |
1450 setmp show_all_types |
1403 (! show_types orelse ! show_sorts orelse ! show_all_types) f; |
1451 (! show_types orelse ! show_sorts orelse ! show_all_types) f; |
1404 |
1452 |
1407 val t2 = @{term "Suc y"}; |
1455 val t2 = @{term "Suc y"}; |
1408 val pty = Pretty.block (Pretty.breaks |
1456 val pty = Pretty.block (Pretty.breaks |
1409 [(setmp show_question_marks false o setmp_show_all_types) |
1457 [(setmp show_question_marks false o setmp_show_all_types) |
1410 (Syntax.pretty_term ctxt) t1, |
1458 (Syntax.pretty_term ctxt) t1, |
1411 Pretty.str "=", Syntax.pretty_term ctxt t2]); |
1459 Pretty.str "=", Syntax.pretty_term ctxt t2]); |
1412 pty |> Pretty.string_of |> priority |
1460 pty |> Pretty.string_of |
1413 *} |
1461 *} |
1414 |
1462 |
1415 text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely *} |
1463 text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely *} |
1416 |
1464 |
1417 |
1465 |
1418 ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> tracing *} |
1466 ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> tracing *} |
1419 ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *} |
1467 ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *} |
1420 |
1468 *) |
1421 |
|
1422 ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of |> tracing *} |
|
1423 ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *} |
|
1424 |
|
1425 text {* |
|
1426 Still to be done: |
|
1427 |
|
1428 What happens with big formulae? |
|
1429 |
|
1430 \begin{readmore} |
|
1431 The general infrastructure for pretty-printing is implemented in the file |
|
1432 @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"} |
|
1433 contains pretty-printing functions for terms, types, theorems and so on. |
|
1434 |
|
1435 @{ML_file "Pure/General/markup.ML"} |
|
1436 \end{readmore} |
|
1437 *} |
|
1438 |
|
1439 text {* |
|
1440 printing into the goal buffer as part of the proof state |
|
1441 *} |
|
1442 |
|
1443 |
|
1444 ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> tracing *} |
|
1445 ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *} |
|
1446 |
|
1447 text {* writing into the goal buffer *} |
|
1448 |
|
1449 ML {* fun my_hook interactive state = |
|
1450 (interactive ? Proof.goal_message (fn () => Pretty.str |
|
1451 "foo")) state |
|
1452 *} |
|
1453 |
|
1454 setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *} |
|
1455 |
|
1456 lemma "False" |
|
1457 oops |
|
1458 |
1469 |
1459 |
1470 |
1460 section {* Misc (TBD) *} |
1471 section {* Misc (TBD) *} |
1461 |
1472 |
1462 ML {*Datatype.get_info @{theory} "List.list"*} |
1473 ML {*Datatype.get_info @{theory} "List.list"*} |