isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:9728b0432fb2
+:0ed6f49277c4
 text {*
 The crucial function @{ML_ind local_theory in Outer_Syntax} expects
 the name for the command, a kind indicator, a short description and
 a parser producing a local theory transition (explained later). For the
 name and the kind, you can use the ML-antiquotation @{text "@{command_spec ...}"}.
-After this, you can write in your theory
+You can now write in your theory
 *}
 foobar
 text {*
-but of course you will not see ``anything''.
+but of course you will not see anything since \isacommand{foobar} is
-Remember that this only works in jEdit. In order to enable also Proof-General
+not intended to do anything.  Remember, however, that this only
-recognise this command, a keyword file needs to be generated (see next
+works in jEdit. In order to enable also Proof-General recognise this
-section).
+command, a keyword file needs to be generated (see next section).
-At the moment the command \isacommand{foobar} is not very useful. Let us
+As it stands, the command \isacommand{foobar} is not very useful. Let
-refine it a bit next by letting it take a proposition as argument and
+us refine it a bit next by letting it take a proposition as argument
-printing this proposition inside the tracing buffer. We announce the
+and printing this proposition inside the tracing buffer. We announce
-command in the theory header as
+the command \isacommand{foobar\_trace} in the theory header as
 \begin{graybox}
 \isacommand{keywords} @{text [quotes] "foobar_trace"} @{text "::"} @{text "thy_decl"}
 \end{graybox}
 apply(rule TrueI)+
 done
 text {*
 The last command we describe here is
-\isacommand{foobar\_proof}. Like \isacommand{lemma}, its purpose is
+\isacommand{foobar\_proof}. Like \isacommand{foobar\_goal}, its purpose is
 to take a proposition and open a corresponding proof-state that
 allows us to give a proof for it. However, unlike
-\isacommand{lemma}, the proposition will be given as a
+\isacommand{foobar\_goal}, the proposition will be given as a
 ML-value. Such a command is quite useful during development
 when you generate a goal on the ML-level and want to see
-whether it is provable. In addition allow the proved
+whether it is provable. In addition we want to allow the proved
 proposition to have a name that can be referenced later on.
-The first problem for this command is to parse some text as
+The first problem for \isacommand{foobar\_proof} is to parse some
-ML-source and then interpret it as an Isabelle term. For the parsing we can
+text as ML-source and then interpret it as an Isabelle term using
-use the function @{ML_ind "ML_source" in Parse} in the structure
+the ML-runtime.  For the parsing part, we can use the function
-@{ML_struct Parse}. For running the ML-interpreter we need the
+@{ML_ind "ML_source" in Parse} in the structure @{ML_struct
-following scaffolding code.
+Parse}. For running the ML-interpreter we need the following
+scaffolding code.
 *}
 ML %grayML{*
-structure Result = Proof_Data (
+structure Result =
-type T = unit -> term
+Proof_Data (type T = unit -> term
 fun init thy () = error "Result")
 val result_cookie = (Result.get, Result.put, "Result.put") *}
 text {*
-With this in place, we can write the code for \isacommand{foobar\_prove}.
+With this in place, we can implement the code for \isacommand{foobar\_prove}
+as follows.
 *}
 ML %linenosgray{*let
 fun after_qed thm_name thms lthy =
 Local_Theory.note (thm_name, (flat thms)) lthy |> snd
 In Line 12, we implement a parser that first reads in an optional lemma name (terminated
 by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML-text
 and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime}
 in the structure @{ML_struct Code_Runtime}.  Once the ML-text has been turned into a term,
 the function @{ML theorem in Proof} opens a corresponding proof-state. This function takes the
-function @{ML_text "after_qed"} as argument, whose purpose is to store the theorem,
+function @{text "after_qed"} as argument, whose purpose is to store the theorem
-once it is proven, under the given name @{text "thm_name"}.
+(once it is proven) under the given name @{text "thm_name"}.
 You can now define a term, for example
 *}
 ML %grayML{*val prop_true = @{prop "True"}*}
 foobar_prove test: prop_true
 apply(rule TrueI)
 done
 text {*
-Finally we can test whether the lemma has been stored under the given name.
+Finally you can test whether the lemma has been stored under the given name.
 \begin{isabelle}
 \isacommand{thm}~@{text "test"}\\
 @{text "> "}~@{thm TrueI}
 \end{isabelle}
 text {*
 Also if the kind of a command changes, from @{text "thy_decl"} to
 @{text "thy_goal"} say,  you need to recreate the keyword file.
 *}
 text {*
 {\bf TBD below}
-(FIXME: read a name and show how to store theorems; see @{ML_ind note in Local_Theory})
+*}
-*}

changeset 522	0ed6f49277c4
parent 521	9728b0432fb2
child 523	0753bc271fd5