diff options
| author | Yves Bertot | 2018-05-02 14:18:39 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-02 14:18:39 +0200 |
| commit | f893ebe4189bb2ecb085e6e139e13c9dadd4611a (patch) | |
| tree | 921478737eeb57c18114c3e9c8e8e3cf0cb2bd70 /tuto1/src | |
| parent | 3df17ed7972dc404cc8519ae9bfd42f75e278e0b (diff) | |
first examples of commands taking arguments
Diffstat (limited to 'tuto1/src')
| -rw-r--r-- | tuto1/src/g_tuto1.ml4 | 24 | ||||
| -rw-r--r-- | tuto1/src/tuto1_plugin.mlpack | 1 |
2 files changed, 25 insertions, 0 deletions
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4 new file mode 100644 index 0000000000..6ff97ae5cf --- /dev/null +++ b/tuto1/src/g_tuto1.ml4 @@ -0,0 +1,24 @@ +open Pp +(* This one is necessary, to avoid message about missing wit_string *) +open Stdarg + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "Hello" string(s)] -> + [ Feedback.msg_notice (strbrk "Hello " ++ str s) ] +END + +(* reference is allowed as a syntactic entry, but so are all the entries + found the signature of module Prim in file coq/parsing/pcoq.mli *) + +VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY +| [ "HelloAgain" reference(r)] -> +(* The function Libnames.pr_reference was found by searchin all mli files + for a function of type reference -> Pp.t *) + [ Feedback.msg_notice + (strbrk "Hello again " ++ Libnames.pr_reference r)] +END + +VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY +| [ "Cmd1" constr(e) ] -> + [ Feedback.msg_notice (strbrk "Cmd1 parsed something") ] +END diff --git a/tuto1/src/tuto1_plugin.mlpack b/tuto1/src/tuto1_plugin.mlpack new file mode 100644 index 0000000000..3b46ea79bf --- /dev/null +++ b/tuto1/src/tuto1_plugin.mlpack @@ -0,0 +1 @@ +G_tuto1
\ No newline at end of file |