|
(** See dev/doc/parsing.md for mlg doc *)
DECLARE PLUGIN "rocq-plugin-tutorial.plugin"
{
open Pp
open Ltac_plugin
let cat = CWarnings.create_category ~name:"plugin-tuto-cat" ()
let tuto_warn = CWarnings.create ~name:"name" ~category:cat
(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.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.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" ] ->
{ CErrors.user_err (str Tuto0_main.message) }
END
[ Dauer der Verarbeitung: 0.38 Sekunden
(vorverarbeitet)
]
|
