102 (* markup *) |
102 (* markup *) |
103 |
103 |
104 local |
104 local |
105 |
105 |
106 val token_kind_markup = |
106 val token_kind_markup = |
107 fn Keyword => Isabelle_Markup.ML_keyword |
107 fn Keyword => (Isabelle_Markup.ML_keyword, "") |
108 | Ident => Markup.empty |
108 | Ident => (Markup.empty, "") |
109 | LongIdent => Markup.empty |
109 | LongIdent => (Markup.empty, "") |
110 | TypeVar => Isabelle_Markup.ML_tvar |
110 | TypeVar => (Isabelle_Markup.ML_tvar, "") |
111 | Word => Isabelle_Markup.ML_numeral |
111 | Word => (Isabelle_Markup.ML_numeral, "") |
112 | Int => Isabelle_Markup.ML_numeral |
112 | Int => (Isabelle_Markup.ML_numeral, "") |
113 | Real => Isabelle_Markup.ML_numeral |
113 | Real => (Isabelle_Markup.ML_numeral, "") |
114 | Char => Isabelle_Markup.ML_char |
114 | Char => (Isabelle_Markup.ML_char, "") |
115 | String => Isabelle_Markup.ML_string |
115 | String => (Isabelle_Markup.ML_string, "") |
116 | Space => Markup.empty |
116 | Space => (Markup.empty, "") |
117 | Comment => Isabelle_Markup.ML_comment |
117 | Comment => (Isabelle_Markup.ML_comment, "") |
118 | Error msg => Isabelle_Markup.bad msg |
118 | Error msg => (Isabelle_Markup.bad, msg) |
119 | EOF => Markup.empty; |
119 | EOF => (Markup.empty, ""); |
120 |
120 |
121 fun token_markup kind x = |
121 fun token_markup kind x = |
122 if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x |
122 if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x |
123 then Isabelle_Markup.ML_delimiter |
123 then (Isabelle_Markup.ML_delimiter, "") |
124 else token_kind_markup kind; |
124 else token_kind_markup kind; |
125 |
125 |
126 in |
126 in |
127 |
127 |
128 fun report_of_token (Token ((pos, _), (kind, x))) = (pos, token_markup kind x); |
128 fun report_of_token (Token ((pos, _), (kind, x))) = |
|
129 let val (markup, txt) = token_markup kind x |
|
130 in ((pos, markup), txt) end; |
129 |
131 |
130 end; |
132 end; |
131 |
133 |
132 |
134 |
133 |
135 |
299 val input = |
301 val input = |
300 (Source.of_list syms |
302 (Source.of_list syms |
301 |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq)) |
303 |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq)) |
302 (SOME (false, fn msg => recover msg >> map Antiquote.Text)) |
304 (SOME (false, fn msg => recover msg >> map Antiquote.Text)) |
303 |> Source.exhaust |
305 |> Source.exhaust |
304 |> tap (Position.reports o Antiquote.reports_of (single o report_of_token)) |
306 |> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token)) |
305 |> tap Antiquote.check_nesting |
307 |> tap Antiquote.check_nesting |
306 |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ()))) |
308 |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ()))) |
307 handle ERROR msg => |
309 handle ERROR msg => |
308 cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos); |
310 cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos); |
309 in input @ termination end; |
311 in input @ termination end; |