[isabelle] Custom Isar Commands



In the first step of building an automatic tool, I am trying to set up
an Isar-level command, following the example of the Nitpick sources.
However, I am having a problem getting Isar to "see" the command.
Here is an utterly simplified version, based on the Nitpick sources.

File test.ml
----------------------------------------

signature TEST =
sig
end

structure Test : TEST =
struct

fun test_function a =
  writeln( "test function called" )
  |> K(K(Toplevel.empty),a)

fun test_params_function a =
  writeln( "test params function called" )
  |> K(K(Toplevel.empty),a)

val _ = Outer_Syntax.improper_command "test"
            "test the Outer_Syntax.improper_command function"
            Keyword.diag test_function
val _ = Outer_Syntax.command "test_params"
            "test the Outer_Syntax.command function"
            Keyword.thy_decl test_params_function

end

------------------------------------
End file test.ml


As far as I can tell, the following Isar code should load the commands
"test" and "test_params" into Isar's syntax:

theory Scratch
imports Main
uses ("test.ml")
begin

use "test.ml"

However, if I next type test or test_params and try to process it,
ProofGeneral will protest that it cannot find any complete commands to
process.
What am I doing wrong here?

Thanks,
Matthew Weidner






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.