Merge PR #10304: Clean up tuto0 and tuto1 to use better practices and explain more

Ack-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
Ack-by: tlringer

1 files changed, 56 insertions, 0 deletions

diff --git a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg
index 5c633fe862..97689adfed 100644
--- a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg
+++ b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg
@@ -5,14 +5,70 @@ DECLARE PLUGIN "tuto0_plugin"
 open Pp
 open Ltac_plugin
 
+let tuto_warn = CWarnings.create ~name:"name" ~category:"category"
+                            (fun _ -> strbrk Tuto0_main.message)
+
 }
 
+(*** Printing messages ***)
+
+(*
+ * This defines a command that prints HelloWorld.
+ * Note that Feedback.msg_notice can be used to print messages.
+ *)
 VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
 | [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) }
 END
 
+(*
+ * This is a tactic version of the same thing.
+ *)
 TACTIC EXTEND hello_world_tactic
 | [ "hello_world" ] ->
   { let _ = Feedback.msg_notice (str Tuto0_main.message) in
     Tacticals.New.tclIDTAC }
 END
+
+(*** Printing warnings ***)
+
+(*
+ * This defines a command that prints HelloWorld as a warning.
+ * tuto_warn is defined at the top-level, before the command runs,
+ * which is standard.
+ *)
+VERNAC COMMAND EXTEND HelloWarning CLASSIFIED AS QUERY
+| [ "HelloWarning" ] ->
+   {
+     tuto_warn ()
+   }
+END
+
+(*
+ * This is a tactic version of the same thing.
+ *)
+TACTIC EXTEND hello_warning_tactic
+| [ "hello_warning" ] ->
+   {
+     let _ = tuto_warn () in
+     Tacticals.New.tclIDTAC
+   }
+END
+
+(*** Printing errors ***)
+
+(*
+ * This defines a command that prints HelloWorld inside of an error.
+ * Note that CErrors.user_err can be used to raise errors to the user.
+ *)
+VERNAC COMMAND EXTEND HelloError CLASSIFIED AS QUERY
+| [ "HelloError" ] -> { CErrors.user_err (str Tuto0_main.message) }
+END
+
+(*
+ * This is a tactic version of the same thing.
+ *)
+TACTIC EXTEND hello_error_tactic
+| [ "hello_error" ] ->
+  { let _ = CErrors.user_err (str Tuto0_main.message) in
+    Tacticals.New.tclIDTAC }
+END