diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 24 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 4 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 13 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 10 |
4 files changed, 25 insertions, 26 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 6a75b99c..821a73f7 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml 11786 2009-01-14 13:07:34Z herbelin $ *) +(* $Id: metasyntax.ml 12882 2010-03-23 22:34:38Z herbelin $ *) open Pp open Util @@ -266,16 +266,18 @@ let split_notation_string str = (* Interpret notations with a recursive component *) -let rec find_pattern xl = function - | Break n as x :: l, Break n' :: l' when n=n' -> - find_pattern (x::xl) (l,l') +let out_nt = function NonTerminal x -> x | _ -> assert false + +let rec find_pattern nt xl = function + | Break n as x :: l, Break n' :: l' when n=n' -> + find_pattern nt (x::xl) (l,l') | Terminal s as x :: l, Terminal s' :: l' when s = s' -> - find_pattern (x::xl) (l,l') - | [NonTerminal x], NonTerminal x' :: l' -> - (x,x',xl),l' - | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ -> + find_pattern nt (x::xl) (l,l') + | [], NonTerminal x' :: l' -> + (out_nt nt,x',List.rev xl),l' + | [], Terminal s :: _ | Terminal s :: _, _ -> error ("The token "^s^" occurs on one side of \"..\" but not on the other side.") - | [NonTerminal _], Break s :: _ | Break s :: _, _ -> + | [], Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") | ((SProdList _ | NonTerminal _) :: _ | []), _ -> error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".") @@ -283,7 +285,8 @@ let rec find_pattern xl = function let rec interp_list_parser hd = function | [] -> [], [], List.rev hd | NonTerminal id :: tl when id = ldots_var -> - let ((x,y,sl),tl') = find_pattern [] (hd,tl) in + let hd = List.rev hd in + let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in let yl,xl,tl'' = interp_list_parser [] tl' in (* We remember each pair of variable denoting a recursive part to *) (* remove the second copy of it afterwards *) @@ -299,6 +302,7 @@ let rec interp_list_parser hd = function yl, xl, List.rev_append hd tl' | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser" + (* Find non-terminal tokens of notation *) let unquote_notation_token s = diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 176f336b..b54700d3 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -11,7 +11,7 @@ * camlp4deps will not work for this file unless Makefile system enhanced. *) -(* $Id: mltop.ml4 11801 2009-01-18 20:11:41Z herbelin $ *) +(* $Id: mltop.ml4 12341 2009-09-17 16:03:19Z glondu $ *) open Util open Pp @@ -109,7 +109,7 @@ let dir_ml_load s = * in this file, the Makefile dependency logic needs to be updated. *) let warn = Flags.is_verbose() in - let _,gname = where_in_path ~warn !coq_mlpath_copy s in + let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in try Dynlink.loadfile gname; with | Dynlink.Error a -> diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index a1acd1d6..9d64f983 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *) +(* $Id: toplevel.ml 12891 2010-03-30 11:40:02Z herbelin $ *) open Pp open Util @@ -163,11 +163,10 @@ let print_location_in_file s inlibrary fname loc = try let (line, bol) = line_of_pos 1 0 0 in close_in ic; - hov 0 - (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str"," ++ spc() ++ - hov 0 (str"line " ++ int line ++ str"," ++ spc() ++ - str"characters " ++ - Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":") ++ + hov 0 (* No line break so as to follow emacs error message format *) + (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ + str", line " ++ int line ++ str", characters " ++ + Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++ fnl () with e -> (close_in ic; @@ -316,7 +315,7 @@ let parse_to_dot = let rec discard_to_dot () = try Gram.Entry.parse parse_to_dot top_buffer.tokens - with Stdpp.Exc_located(_,Token.Error _) -> + with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) -> discard_to_dot() diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6a0acb52..385afbec 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 12187 2009-06-13 19:36:59Z msozeau $ i*) +(*i $Id: vernacentries.ml 12343 2009-09-17 17:02:03Z glondu $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -234,12 +234,8 @@ let dump_universes s = (* "Locate" commands *) let locate_file f = - try - let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in - msgnl (str file) - with Not_found -> - msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++ - str"on loadpath")) + let _,file = System.find_file_in_path ~warn:false (Library.get_load_paths ()) f in + msgnl (str file) let msg_found_library = function | Library.LibLoaded, fulldir, file -> |