559 OuterParse.term input |
559 OuterParse.term input |
560 end" |
560 end" |
561 "(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"} |
561 "(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"} |
562 |
562 |
563 The function @{ML OuterParse.prop} is similar, except that it gives a different |
563 The function @{ML OuterParse.prop} is similar, except that it gives a different |
564 error message, when parsing fails. Looking closer at the result string you will |
564 error message, when parsing fails. As you can see, the parser not just returns |
565 have noticed that the parser not just returns the parsed string, but also some |
565 the parsed string, but also some encoded information. You can decode the |
566 encoded information. You can see this better if you replace |
566 information with the function @{ML YXML.parse}. For example |
567 @{ML Position.none} by @{ML "(Position.line 42)"}, say. |
567 |
|
568 @{ML_response [display,gray] |
|
569 "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\"" |
|
570 "XML.Elem (\"token\", [], [XML.Text \"foo\"])"} |
|
571 |
|
572 You can see better what is going on if you replace |
|
573 @{ML Position.none} by @{ML "Position.line 42"}, say: |
568 |
574 |
569 @{ML_response [display,gray] |
575 @{ML_response [display,gray] |
570 "let |
576 "let |
571 val input = OuterSyntax.scan (Position.line 42) \"foo\" |
577 val input = OuterSyntax.scan (Position.line 42) \"foo\" |
572 in |
578 in |
573 OuterParse.term input |
579 YXML.parse (fst (OuterParse.term input)) |
574 end" |
580 end" |
575 "(\"\\^E\\^Ftoken\\^Fline=42\\^Fend_line=42\\^Efoo\\^E\\^F\\^E\", [])"} |
581 "XML.Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"} |
576 |
582 |
577 The positional information is stored so that code called later on will be |
583 The positional information is stored so that code called later on will be |
578 able to give more precise error messages. |
584 able to give more precise error messages. |
579 |
585 |
580 *} |
586 \begin{readmore} |
|
587 The functions to do with input and outout of XML and YXML are defined |
|
588 in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}. |
|
589 \end{readmore} |
|
590 *} |
|
591 |
581 |
592 |
582 section {* Parsing Specifications\label{sec:parsingspecs} *} |
593 section {* Parsing Specifications\label{sec:parsingspecs} *} |
583 |
594 |
584 text {* |
595 text {* |
585 There are a number of special purpose parsers that help with parsing |
596 There are a number of special purpose parsers that help with parsing |
705 (name, map Args.dest_src attrib) |
716 (name, map Args.dest_src attrib) |
706 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"} |
717 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"} |
707 |
718 |
708 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of |
719 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of |
709 @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some |
720 @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some |
710 attributes. If you want to print out all currently known attributes a theorem |
721 attributes. |
711 can have, you can use the function: |
|
712 |
|
713 @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" |
|
714 "COMP: direct composition with rules (no lifting) |
|
715 HOL.dest: declaration of Classical destruction rule |
|
716 HOL.elim: declaration of Classical elimination rule |
|
717 \<dots>"} |
|
718 |
|
719 |
722 |
720 For the inductive definitions described above only the attibutes @{text "[intro]"} and |
723 For the inductive definitions described above only the attibutes @{text "[intro]"} and |
721 @{text "[simp]"} make sense. |
724 @{text "[simp]"} make sense. |
722 |
725 |
723 \begin{readmore} |
726 \begin{readmore} |