author | wenzelm |
Tue, 05 Dec 2017 14:03:10 +0100 | |
changeset 67136 | 1368cfa92b7a |
parent 64556 | 851ae0e7b09c |
child 67439 | 78759a7bd874 |
permissions | -rw-r--r-- |
5829 | 1 |
(* Title: Pure/Isar/outer_syntax.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
4 |
Isabelle/Isar outer syntax. |
5829 | 5 |
*) |
6 |
||
7 |
signature OUTER_SYNTAX = |
|
8 |
sig |
|
58930 | 9 |
val help: theory -> string list -> unit |
10 |
val print_commands: theory -> unit |
|
59935 | 11 |
type command_keyword = string * Position.T |
12 |
val command: command_keyword -> string -> |
|
29311 | 13 |
(Toplevel.transition -> Toplevel.transition) parser -> unit |
63273 | 14 |
val maybe_begin_local_theory: command_keyword -> string -> |
15 |
(local_theory -> local_theory) parser -> (theory -> local_theory) parser -> unit |
|
59935 | 16 |
val local_theory': command_keyword -> string -> |
29380 | 17 |
(bool -> local_theory -> local_theory) parser -> unit |
59935 | 18 |
val local_theory: command_keyword -> string -> |
29311 | 19 |
(local_theory -> local_theory) parser -> unit |
59935 | 20 |
val local_theory_to_proof': command_keyword -> string -> |
29311 | 21 |
(bool -> local_theory -> Proof.state) parser -> unit |
59935 | 22 |
val local_theory_to_proof: command_keyword -> string -> |
29311 | 23 |
(local_theory -> Proof.state) parser -> unit |
60095 | 24 |
val bootstrap: bool Config.T |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
25 |
val parse: theory -> Position.T -> string -> Toplevel.transition list |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
26 |
val parse_tokens: theory -> Token.T list -> Toplevel.transition list |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
27 |
val parse_spans: Token.T list -> Command_Span.span list |
52510 | 28 |
val side_comments: Token.T list -> Token.T list |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
29 |
val command_reports: theory -> Token.T -> Position.report_text list |
63274 | 30 |
val check_command: Proof.context -> command_keyword -> string |
5829 | 31 |
end; |
32 |
||
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
33 |
structure Outer_Syntax: OUTER_SYNTAX = |
5829 | 34 |
struct |
35 |
||
36 |
(** outer syntax **) |
|
37 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
38 |
(* errors *) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
39 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
40 |
fun err_command msg name ps = |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
41 |
error (msg ^ quote (Markup.markup Markup.keyword1 name) ^ Position.here_list ps); |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
42 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
43 |
fun err_dup_command name ps = |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
44 |
err_command "Duplicate outer syntax command " name ps; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
45 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
46 |
|
29311 | 47 |
(* command parsers *) |
5829 | 48 |
|
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
49 |
datatype command_parser = |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
50 |
Parser of (Toplevel.transition -> Toplevel.transition) parser | |
60691 | 51 |
Restricted_Parser of |
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59935
diff
changeset
|
52 |
(bool * Position.T) option -> (Toplevel.transition -> Toplevel.transition) parser; |
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
53 |
|
29311 | 54 |
datatype command = Command of |
24868 | 55 |
{comment: string, |
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
56 |
command_parser: command_parser, |
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
57 |
pos: Position.T, |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
58 |
id: serial}; |
5829 | 59 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
60 |
fun eq_command (Command {id = id1, ...}, Command {id = id2, ...}) = id1 = id2; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
61 |
|
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
62 |
fun new_command comment command_parser pos = |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
63 |
Command {comment = comment, command_parser = command_parser, pos = pos, id = serial ()}; |
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
64 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
65 |
fun command_pos (Command {pos, ...}) = pos; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
66 |
|
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
67 |
fun command_markup def (name, Command {pos, id, ...}) = |
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
68 |
Markup.properties (Position.entity_properties_of def id pos) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49564
diff
changeset
|
69 |
(Markup.entity Markup.commandN name); |
5829 | 70 |
|
50213 | 71 |
fun pretty_command (cmd as (name, Command {comment, ...})) = |
72 |
Pretty.block |
|
73 |
(Pretty.marks_str |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
74 |
([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]}, |
50215 | 75 |
command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); |
50213 | 76 |
|
5829 | 77 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
78 |
(* theory data *) |
43711 | 79 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
80 |
structure Data = Theory_Data |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
81 |
( |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
82 |
type T = command Symtab.table; |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
83 |
val empty = Symtab.empty; |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
84 |
val extend = I; |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
85 |
fun merge data : T = |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
86 |
data |> Symtab.join (fn name => fn (cmd1, cmd2) => |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
87 |
if eq_command (cmd1, cmd2) then raise Symtab.SAME |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
88 |
else err_dup_command name [command_pos cmd1, command_pos cmd2]); |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
89 |
); |
43711 | 90 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
91 |
val get_commands = Data.get; |
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
60693
diff
changeset
|
92 |
val dest_commands = get_commands #> Symtab.dest #> sort_by #1; |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
93 |
val lookup_commands = Symtab.lookup o get_commands; |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
94 |
|
58930 | 95 |
fun help thy pats = |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
96 |
dest_commands thy |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
97 |
|> filter (fn (name, _) => forall (fn pat => match_string pat name) pats) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
98 |
|> map pretty_command |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
99 |
|> Pretty.writeln_chunks; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
100 |
|
58930 | 101 |
fun print_commands thy = |
43711 | 102 |
let |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
103 |
val keywords = Thy_Header.get_keywords thy; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
104 |
val minor = Scan.dest_lexicon (Keyword.minor_keywords keywords); |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
105 |
val commands = dest_commands thy; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
106 |
in |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
107 |
[Pretty.strs ("keywords:" :: map quote minor), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
108 |
Pretty.big_list "commands:" (map pretty_command commands)] |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
109 |
|> Pretty.writeln_chunks |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
110 |
end; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
111 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
112 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
113 |
(* maintain commands *) |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
114 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
115 |
fun add_command name cmd thy = |
63022 | 116 |
if member (op =) Thy_Header.bootstrap_thys (Context.theory_name thy) then thy |
117 |
else |
|
118 |
let |
|
119 |
val _ = |
|
120 |
Keyword.is_command (Thy_Header.get_keywords thy) name orelse |
|
121 |
err_command "Undeclared outer syntax command " name [command_pos cmd]; |
|
122 |
val _ = |
|
123 |
(case lookup_commands thy name of |
|
124 |
NONE => () |
|
125 |
| SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']); |
|
126 |
val _ = |
|
127 |
Context_Position.report_generic (Context.the_generic_context ()) |
|
128 |
(command_pos cmd) (command_markup true (name, cmd)); |
|
129 |
in Data.map (Symtab.update (name, cmd)) thy end; |
|
43711 | 130 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
131 |
val _ = Theory.setup (Theory.at_end (fn thy => |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
132 |
let |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
133 |
val command_keywords = |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
134 |
Scan.dest_lexicon (Keyword.major_keywords (Thy_Header.get_keywords thy)); |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
135 |
val _ = |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58934
diff
changeset
|
136 |
(case subtract (op =) (map #1 (dest_commands thy)) command_keywords of |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
137 |
[] => () |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
138 |
| missing => error ("Missing outer syntax command(s) " ^ commas_quote missing)) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
139 |
in NONE end)); |
43711 | 140 |
|
5829 | 141 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
142 |
(* implicit theory setup *) |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
143 |
|
59935 | 144 |
type command_keyword = string * Position.T; |
5952 | 145 |
|
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
146 |
fun raw_command (name, pos) comment command_parser = |
59932 | 147 |
let val setup = add_command name (new_command comment command_parser pos) |
148 |
in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end; |
|
26990 | 149 |
|
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
150 |
fun command (name, pos) comment parse = |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
151 |
raw_command (name, pos) comment (Parser parse); |
59923
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59083
diff
changeset
|
152 |
|
63273 | 153 |
fun maybe_begin_local_theory command_keyword comment parse_local parse_global = |
154 |
raw_command command_keyword comment |
|
155 |
(Restricted_Parser (fn restricted => |
|
156 |
Parse.opt_target -- parse_local |
|
157 |
>> (fn (target, f) => Toplevel.local_theory restricted target f) || |
|
158 |
(if is_some restricted then Scan.fail |
|
159 |
else parse_global >> Toplevel.begin_local_theory true))); |
|
160 |
||
59935 | 161 |
fun local_theory_command trans command_keyword comment parse = |
162 |
raw_command command_keyword comment |
|
60691 | 163 |
(Restricted_Parser (fn restricted => |
164 |
Parse.opt_target -- parse >> (fn (target, f) => trans restricted target f))); |
|
26990 | 165 |
|
56895
f058120aaad4
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents:
56334
diff
changeset
|
166 |
val local_theory' = local_theory_command Toplevel.local_theory'; |
f058120aaad4
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents:
56334
diff
changeset
|
167 |
val local_theory = local_theory_command Toplevel.local_theory; |
f058120aaad4
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents:
56334
diff
changeset
|
168 |
val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof'; |
f058120aaad4
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents:
56334
diff
changeset
|
169 |
val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof; |
26990 | 170 |
|
171 |
||
5829 | 172 |
|
9132 | 173 |
(** toplevel parsing **) |
5829 | 174 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
175 |
(* parse commands *) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
176 |
|
60095 | 177 |
val bootstrap = |
64556 | 178 |
Config.bool (Config.declare ("Outer_Syntax.bootstrap", \<^here>) (K (Config.Bool true))); |
60095 | 179 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
180 |
local |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
181 |
|
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59935
diff
changeset
|
182 |
val before_command = |
59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset
|
183 |
Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false)); |
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59935
diff
changeset
|
184 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
185 |
fun parse_command thy = |
67136 | 186 |
Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) => |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
187 |
let |
60693
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60691
diff
changeset
|
188 |
val keywords = Thy_Header.get_keywords thy; |
67136 | 189 |
val command_tags = Parse.command -- Parse.tags; |
60693
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60691
diff
changeset
|
190 |
val tr0 = |
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60691
diff
changeset
|
191 |
Toplevel.empty |
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60691
diff
changeset
|
192 |
|> Toplevel.name name |
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60691
diff
changeset
|
193 |
|> Toplevel.position pos |
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60691
diff
changeset
|
194 |
|> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open |
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60691
diff
changeset
|
195 |
|> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close; |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
196 |
in |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
197 |
(case lookup_commands thy name of |
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
198 |
SOME (Command {command_parser = Parser parse, ...}) => |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
199 |
Parse.!!! (command_tags |-- parse) >> (fn f => f tr0) |
60691 | 200 |
| SOME (Command {command_parser = Restricted_Parser parse, ...}) => |
201 |
before_command :|-- (fn restricted => |
|
202 |
Parse.!!! (command_tags |-- parse restricted)) >> (fn f => f tr0) |
|
60095 | 203 |
| NONE => |
204 |
Scan.fail_with (fn _ => fn _ => |
|
205 |
let |
|
206 |
val msg = |
|
207 |
if Config.get_global thy bootstrap |
|
208 |
then "missing theory context for command " |
|
209 |
else "undefined command "; |
|
210 |
in msg ^ quote (Markup.markup Markup.keyword1 name) end)) |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
211 |
end); |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
212 |
|
61579 | 213 |
val parse_cmt = (Parse.$$$ "--" || Parse.$$$ Symbol.comment) -- Parse.!!! Parse.document_source; |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
214 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
215 |
fun commands_source thy = |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
216 |
Token.source_proper #> |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
217 |
Source.source Token.stopper (Scan.bulk (parse_cmt >> K NONE || Parse.not_eof >> SOME)) #> |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
218 |
Source.map_filter I #> |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
219 |
Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs)); |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
220 |
|
60073
76a8400a58d9
more robust error handling of commands that are declared but not yet defined;
wenzelm
parents:
59990
diff
changeset
|
221 |
in |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
222 |
|
63936 | 223 |
fun parse thy pos = |
224 |
Symbol.explode |
|
225 |
#> Source.of_list |
|
226 |
#> Token.source (Thy_Header.get_keywords thy) pos |
|
227 |
#> commands_source thy |
|
228 |
#> Source.exhaust; |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
229 |
|
63936 | 230 |
fun parse_tokens thy = |
231 |
Source.of_list |
|
232 |
#> commands_source thy |
|
233 |
#> Source.exhaust; |
|
57918
f5d73caba4e5
tuned signature according to Scala version -- prefer explicit argument;
wenzelm
parents:
57905
diff
changeset
|
234 |
|
60073
76a8400a58d9
more robust error handling of commands that are declared but not yet defined;
wenzelm
parents:
59990
diff
changeset
|
235 |
end; |
76a8400a58d9
more robust error handling of commands that are declared but not yet defined;
wenzelm
parents:
59990
diff
changeset
|
236 |
|
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
237 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
238 |
(* parse spans *) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
239 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
240 |
local |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
241 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
242 |
fun ship span = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
243 |
let |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
244 |
val kind = |
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
245 |
if forall Token.is_improper span then Command_Span.Ignored_Span |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
246 |
else if exists Token.is_error span then Command_Span.Malformed_Span |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
247 |
else |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
248 |
(case find_first Token.is_command span of |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
249 |
NONE => Command_Span.Malformed_Span |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
250 |
| SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd)); |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
251 |
in cons (Command_Span.Span (kind, span)) end; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
252 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
253 |
fun flush (result, content, improper) = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
254 |
result |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
255 |
|> not (null content) ? ship (rev content) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
256 |
|> not (null improper) ? ship (rev improper); |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
257 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
258 |
fun parse tok (result, content, improper) = |
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
259 |
if Token.is_improper tok then (result, content, tok :: improper) |
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59935
diff
changeset
|
260 |
else if Token.is_command_modifier tok orelse |
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
261 |
Token.is_command tok andalso |
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59935
diff
changeset
|
262 |
(not (exists Token.is_command_modifier content) orelse exists Token.is_command content) |
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59923
diff
changeset
|
263 |
then (flush (result, content, improper), [tok], []) |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
264 |
else (result, tok :: (improper @ content), []); |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
265 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
266 |
in |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
267 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
268 |
fun parse_spans toks = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
269 |
fold parse toks ([], [], []) |> flush |> rev; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
270 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
271 |
end; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57623
diff
changeset
|
272 |
|
14091 | 273 |
|
52510 | 274 |
(* side-comments *) |
48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
275 |
|
52510 | 276 |
fun cmts (t1 :: t2 :: toks) = |
61579 | 277 |
if Token.keyword_with (fn s => s = "--" orelse s = Symbol.comment) t1 then t2 :: cmts toks |
52510 | 278 |
else cmts (t2 :: toks) |
279 |
| cmts _ = []; |
|
280 |
||
281 |
val side_comments = filter Token.is_proper #> cmts; |
|
282 |
||
283 |
||
61618
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
284 |
(* check commands *) |
48647
a5144c4c26a2
report commands as formal entities, with def/ref positions;
wenzelm
parents:
48646
diff
changeset
|
285 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
286 |
fun command_reports thy tok = |
52510 | 287 |
if Token.is_command tok then |
288 |
let val name = Token.content_of tok in |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
289 |
(case lookup_commands thy name of |
52510 | 290 |
NONE => [] |
55708 | 291 |
| SOME cmd => [((Token.pos_of tok, command_markup false (name, cmd)), "")]) |
52510 | 292 |
end |
293 |
else []; |
|
48749
c197b3c3e7fa
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents:
48647
diff
changeset
|
294 |
|
61618
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
295 |
fun check_command ctxt (name, pos) = |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
296 |
let |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
297 |
val thy = Proof_Context.theory_of ctxt; |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
298 |
val keywords = Thy_Header.get_keywords thy; |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
299 |
in |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
300 |
if Keyword.is_command keywords name then |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
301 |
let |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
302 |
val markup = |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
303 |
Token.explode keywords Position.none name |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
304 |
|> maps (command_reports thy) |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
305 |
|> map (#2 o #1); |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
306 |
val _ = Context_Position.reports ctxt (map (pair pos) markup); |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
307 |
in name end |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
308 |
else |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
309 |
let |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
310 |
val completion = |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
311 |
Completion.make (name, pos) |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
312 |
(fn completed => |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
313 |
Keyword.dest_commands keywords |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
314 |
|> filter completed |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
315 |
|> sort_strings |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
316 |
|> map (fn a => (a, (Markup.commandN, a)))); |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
317 |
val report = Markup.markup_report (Completion.reported_text completion); |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
318 |
in error ("Bad command " ^ quote name ^ Position.here pos ^ report) end |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
319 |
end; |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
61579
diff
changeset
|
320 |
|
62849
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
61618
diff
changeset
|
321 |
|
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
61618
diff
changeset
|
322 |
(* 'ML' command -- required for bootstrapping Isar *) |
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
61618
diff
changeset
|
323 |
|
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
61618
diff
changeset
|
324 |
val _ = |
64556 | 325 |
command ("ML", \<^here>) "ML text within theory or local theory" |
62849
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
61618
diff
changeset
|
326 |
(Parse.ML_source >> (fn source => |
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
61618
diff
changeset
|
327 |
Toplevel.generic_theory |
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
61618
diff
changeset
|
328 |
(ML_Context.exec (fn () => |
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
61618
diff
changeset
|
329 |
ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #> |
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
61618
diff
changeset
|
330 |
Local_Theory.propagate_ml_env))); |
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
61618
diff
changeset
|
331 |
|
5829 | 332 |
end; |