From f893ebe4189bb2ecb085e6e139e13c9dadd4611a Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 2 May 2018 14:18:39 +0200
Subject: first examples of commands taking arguments

---
 tuto1/Makefile                | 14 ++++++++++++++
 tuto1/_CoqProject             |  5 +++++
 tuto1/src/g_tuto1.ml4         | 24 ++++++++++++++++++++++++
 tuto1/src/tuto1_plugin.mlpack |  1 +
 4 files changed, 44 insertions(+)
 create mode 100644 tuto1/Makefile
 create mode 100644 tuto1/_CoqProject
 create mode 100644 tuto1/src/g_tuto1.ml4
 create mode 100644 tuto1/src/tuto1_plugin.mlpack

diff --git a/tuto1/Makefile b/tuto1/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/tuto1/Makefile
@@ -0,0 +1,14 @@
+ifeq "$(COQBIN)" ""
+  COQBIN=$(dir $(shell which coqtop))/
+endif
+
+%: Makefile.coq
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+tests: all
+	@$(MAKE) -C tests -s clean
+	@$(MAKE) -C tests -s all
+
+-include Makefile.coq
diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject
new file mode 100644
index 0000000000..7a191a961d
--- /dev/null
+++ b/tuto1/_CoqProject
@@ -0,0 +1,5 @@
+-R theories/ Tuto0
+-I src
+
+src/g_tuto1.ml4
+src/tuto1_plugin.mlpack
\ No newline at end of file
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
-- 
cgit v1.2.3