diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 8 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 9 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 13 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 6 |
4 files changed, 27 insertions, 9 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index d1e379cca..c6e694902 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -44,6 +44,11 @@ let explain_exn_default = function hov 0 ((if loc = Loc.ghost then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ Errors.print_no_anomaly exc) + | Compat.Exc_located (loc, exc) -> + let loc = Compat.to_coqloc loc in + hov 0 ((if loc = Loc.ghost then (mt ()) + else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) + ++ Errors.print_no_anomaly exc) | EvaluatedError (msg,None) -> msg | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise (* Otherwise, not handled here *) @@ -110,6 +115,9 @@ let rec process_vernac_interp_error = function Some (process_vernac_interp_error exc)) | Loc.Exc_located (loc,exc) -> Loc.Exc_located (loc,process_vernac_interp_error exc) + | Compat.Exc_located (loc, exc) -> + let loc = Compat.to_coqloc loc in + Loc.Exc_located (loc, process_vernac_interp_error exc) | exc -> exc diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 8bfcfea6a..bd426b6fd 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -292,8 +292,13 @@ let eval_call c = | Errors.Quit -> None, "Quit is not allowed by coqide!" | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner | Error_in_file (_,_,inner) -> None, pr_exn inner - | Loc.Exc_located (loc, inner) when loc = Loc.ghost -> None, pr_exn inner - | Loc.Exc_located (loc, inner) -> Some (Loc.unloc loc), pr_exn inner + | Loc.Exc_located (loc, inner) -> + let loc = if loc = Loc.ghost then None else Some (Loc.unloc loc) in + loc, pr_exn inner + | Compat.Exc_located (loc, inner) -> + let loc = Compat.to_coqloc loc in + let loc = if loc = Loc.ghost then None else Some (Loc.unloc loc) in + loc, pr_exn inner | e -> None, pr_exn e in let interruptible f x = diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a665dc373..d406bf8d9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -24,7 +24,6 @@ open Vernacexpr open Pcoq open Libnames open Tok -open Lexer open Egramml open Egramcoq open Notation @@ -33,7 +32,7 @@ open Nameops (**********************************************************************) (* Tokens *) -let cache_token (_,s) = add_keyword s +let cache_token (_,s) = Lexer.add_keyword s let inToken : string -> obj = declare_object {(default_object "TOKEN") with @@ -159,7 +158,7 @@ let pr_grammar = function (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) -let parse_format (loc,str) = +let parse_format ((loc, str) : lstring) = let str = " "^str in let l = String.length str in let push_token a = function @@ -334,7 +333,7 @@ let rec interp_list_parser hd = function (* To protect alphabetic tokens and quotes from being seen as variables *) let quote_notation_token x = let n = String.length x in - let norm = is_ident x in + let norm = Lexer.is_ident x in if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'" else x @@ -342,7 +341,7 @@ let rec raw_analyze_notation_tokens = function | [] -> [] | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl | String "_" :: _ -> error "_ must be quoted." - | String x :: sl when is_ident x -> + | String x :: sl when Lexer.is_ident x -> NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl | String s :: sl -> Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens sl @@ -643,12 +642,12 @@ let make_production etyps symbols = let typ = List.assoc m etyps in distribute [GramConstrNonTerminal (typ, Some m)] ll | Terminal s -> - distribute [GramConstrTerminal (terminal s)] ll + distribute [GramConstrTerminal (Lexer.terminal s)] ll | Break _ -> ll | SProdList (x,sl) -> let tkl = List.flatten - (List.map (function Terminal s -> [terminal s] + (List.map (function Terminal s -> [Lexer.terminal s] | Break _ -> [] | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in match List.assoc x etyps with diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 74ed231d1..7e301ba0e 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -291,6 +291,12 @@ let print_toplevel_error exc = (print_highlight_location top_buffer loc, ie) else ((mt ()) (* print_command_location top_buffer dloc *), ie) + | Compat.Exc_located (loc, ie) -> + let loc = Compat.to_coqloc loc in + if valid_buffer_loc top_buffer dloc loc then + (print_highlight_location top_buffer loc, ie) + else + ((mt ()) (* print_command_location top_buffer dloc *), ie) | Error_in_file (s, (inlibrary, fname, loc), ie) -> (print_location_in_file s inlibrary fname loc, ie) | _ -> |