blob: 97689adfed293291bddc3b5187bf7b784489f8b5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
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
|
