ProgTutorial/Parsing.thy
changeset 394 0019ebf76e10
parent 392 47e5b71c7f6c
child 397 6b423b39cc11
equal deleted inserted replaced
393:d8b6d5003823 394:0019ebf76e10
   937   at all. We shall name this command \isacommand{foobar}. On the ML-level it can be 
   937   at all. We shall name this command \isacommand{foobar}. On the ML-level it can be 
   938   defined as:
   938   defined as:
   939 *}
   939 *}
   940 
   940 
   941 ML{*let
   941 ML{*let
   942   val do_nothing = Scan.succeed (LocalTheory.theory I)
   942   val do_nothing = Scan.succeed (Local_Theory.theory I)
   943   val kind = OuterKeyword.thy_decl
   943   val kind = OuterKeyword.thy_decl
   944 in
   944 in
   945   OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
   945   OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
   946 end *}
   946 end *}
   947 
   947 
   974   \isacommand{imports}~@{text Main}\\
   974   \isacommand{imports}~@{text Main}\\
   975   \isacommand{begin}\\
   975   \isacommand{begin}\\
   976   \isacommand{ML}~@{text "\<verbopen>"}\\
   976   \isacommand{ML}~@{text "\<verbopen>"}\\
   977   @{ML
   977   @{ML
   978 "let
   978 "let
   979   val do_nothing = Scan.succeed (LocalTheory.theory I)
   979   val do_nothing = Scan.succeed (Local_Theory.theory I)
   980   val kind = OuterKeyword.thy_decl
   980   val kind = OuterKeyword.thy_decl
   981 in
   981 in
   982   OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
   982   OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
   983 end"}\\
   983 end"}\\
   984   @{text "\<verbclose>"}\\
   984   @{text "\<verbclose>"}\\
  1091   printing this proposition inside the tracing buffer.
  1091   printing this proposition inside the tracing buffer.
  1092 
  1092 
  1093   The crucial part of a command is the function that determines the behaviour
  1093   The crucial part of a command is the function that determines the behaviour
  1094   of the command. In the code above we used a ``do-nothing''-function, which
  1094   of the command. In the code above we used a ``do-nothing''-function, which
  1095   because of @{ML_ind succeed in Scan} does not parse any argument, but immediately
  1095   because of @{ML_ind succeed in Scan} does not parse any argument, but immediately
  1096   returns the simple function @{ML "LocalTheory.theory I"}. We can
  1096   returns the simple function @{ML "Local_Theory.theory I"}. We can
  1097   replace this code by a function that first parses a proposition (using the
  1097   replace this code by a function that first parses a proposition (using the
  1098   parser @{ML OuterParse.prop}), then prints out the tracing
  1098   parser @{ML OuterParse.prop}), then prints out the tracing
  1099   information (using a new function @{text trace_prop}) and 
  1099   information (using a new function @{text trace_prop}) and 
  1100   finally does nothing. For this you can write:
  1100   finally does nothing. For this you can write:
  1101 *}
  1101 *}
  1102 
  1102 
  1103 ML{*let
  1103 ML{*let
  1104   fun trace_prop str = 
  1104   fun trace_prop str = 
  1105      LocalTheory.theory (fn ctxt => (tracing str; ctxt))
  1105      Local_Theory.theory (fn ctxt => (tracing str; ctxt))
  1106 
  1106 
  1107   val kind = OuterKeyword.thy_decl
  1107   val kind = OuterKeyword.thy_decl
  1108 in
  1108 in
  1109   OuterSyntax.local_theory "foobar_trace" "traces a proposition" 
  1109   OuterSyntax.local_theory "foobar_trace" "traces a proposition" 
  1110     kind (OuterParse.prop >> trace_prop)
  1110     kind (OuterParse.prop >> trace_prop)
  1179 done
  1179 done
  1180 
  1180 
  1181 text {*
  1181 text {*
  1182   {\bf TBD below}
  1182   {\bf TBD below}
  1183 
  1183 
  1184   (FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory})
  1184   (FIXME: read a name and show how to store theorems; see @{ML_ind note in Local_Theory})
  1185   
  1185   
  1186 *}
  1186 *}
  1187 
  1187 
  1188 ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*}
  1188 ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*}
  1189 ML{*let
  1189 ML{*let
  1190    fun after_qed thm_name thms lthy =
  1190    fun after_qed thm_name thms lthy =
  1191         LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd
  1191         Local_Theory.note (thm_name, (flat thms)) lthy |> snd
  1192 
  1192 
  1193    fun setup_proof (thm_name, (txt, pos)) lthy =
  1193    fun setup_proof (thm_name, (txt, pos)) lthy =
  1194    let
  1194    let
  1195      val trm = ML_Context.evaluate lthy true ("r", r) txt
  1195      val trm = ML_Context.evaluate lthy true ("r", r) txt
  1196    in
  1196    in