546  Token (\<dots>,(Keyword, \"|\"),\<dots>), 

   546  Token (\<dots>,(Keyword, \"|\"),\<dots>), 

   547  Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}

   547  Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}

   548 

   548 

   549   you obtain a list consisting of only one command and two keyword tokens.

   549   you obtain a list consisting of only one command and two keyword tokens.

   550   If you want to see which keywords and commands are currently known to Isabelle, 

   550   If you want to see which keywords and commands are currently known to Isabelle, 

   552 

   552 

   553 @{ML_response_fake [display,gray] 

   553 @{ML_response_fake [display,gray] 

   554 "let 

   554 "let 

   555   val (keywords, commands) = Keyword.get_lexicons ()

   555   val (keywords, commands) = Keyword.get_lexicons ()

   556 in 

   556 in 

   954   at all. We shall name this command \isacommand{foobar}. On the ML-level it can be 

   954   at all. We shall name this command \isacommand{foobar}. On the ML-level it can be 

   955   defined as:

   955   defined as:

   956 *}

   956 *}

   957 

   957 

   958 ML{*let

   958 ML{*let

   960   val kind = Keyword.thy_decl

   960   val kind = Keyword.thy_decl

   961 in

   961 in

   962   Outer_Syntax.local_theory "foobar" "description of foobar" kind do_nothing

   962   Outer_Syntax.local_theory "foobar" "description of foobar" kind do_nothing

   963 end *}

   963 end *}

   964 

   964 

   991   \isacommand{imports}~@{text Main}\\

   991   \isacommand{imports}~@{text Main}\\

   992   \isacommand{begin}\\

   992   \isacommand{begin}\\

   993   \isacommand{ML}~@{text "\<verbopen>"}\\

   993   \isacommand{ML}~@{text "\<verbopen>"}\\

   994   @{ML

   994   @{ML

   995 "let

   995 "let

   997   val kind = Keyword.thy_decl

   997   val kind = Keyword.thy_decl

   998 in

   998 in

   999   Outer_Syntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing

   999   Outer_Syntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing

  1000 end"}\\

  1000 end"}\\

  1001   @{text "\<verbclose>"}\\

  1001   @{text "\<verbclose>"}\\

  1108   printing this proposition inside the tracing buffer.

  1108   printing this proposition inside the tracing buffer.

  1109 

  1109 

  1110   The crucial part of a command is the function that determines the behaviour

  1110   The crucial part of a command is the function that determines the behaviour

  1111   of the command. In the code above we used a ``do-nothing''-function, which

  1111   of the command. In the code above we used a ``do-nothing''-function, which

  1112   because of @{ML_ind succeed in Scan} does not parse any argument, but immediately

  1112   because of @{ML_ind succeed in Scan} does not parse any argument, but immediately

  1114   replace this code by a function that first parses a proposition (using the

  1114   replace this code by a function that first parses a proposition (using the

  1115   parser @{ML Parse.prop}), then prints out the tracing

  1115   parser @{ML Parse.prop}), then prints out the tracing

  1116   information (using a new function @{text trace_prop}) and 

  1116   information (using a new function @{text trace_prop}) and 

  1117   finally does nothing. For this you can write:

  1117   finally does nothing. For this you can write:

  1118 *}

  1118 *}

  1119 

  1119 

  1120 ML{*let

  1120 ML{*let

  1121   fun trace_prop str = 

  1121   fun trace_prop str = 

  1123 

  1123 

  1124   val kind = Keyword.thy_decl

  1124   val kind = Keyword.thy_decl

  1125 in

  1125 in

  1126   Outer_Syntax.local_theory "foobar_trace" "traces a proposition" 

  1126   Outer_Syntax.local_theory "foobar_trace" "traces a proposition" 

  1127     kind (Parse.prop >> trace_prop)

  1127     kind (Parse.prop >> trace_prop)