diff options
| -rw-r--r-- | interp/constrintern.ml | 52 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 6 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 18 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 45 |
4 files changed, 63 insertions, 58 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 805ffba42..57b5762d7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -129,9 +129,9 @@ type coqdoc_state = Lexer.location_table * int * int let coqdoc_freeze () = let lt = Lexer.location_table() in let state = (lt,!token_number,!last_pos) in - token_number := 0; - last_pos := 0; - state + token_number := 0; + last_pos := 0; + state let coqdoc_unfreeze (lt,tn,lp) = Lexer.restore_location_table lt; @@ -145,7 +145,7 @@ let add_glob loc ref = let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in let filepath = string_of_dirpath lib_dp in let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in - dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname) + dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname) let loc_of_notation f loc args ntn = if args=[] or ntn.[0] <> '_' then fst (unloc loc) @@ -158,15 +158,15 @@ let dump_notation_location pos ((path,df),sc) = let rec next growing = let loc = Lexer.location_function !token_number in let (bp,_) = unloc loc in - if growing then if bp >= pos then loc else (incr token_number;next true) - else if bp = pos then loc - else if bp > pos then (decr token_number;next false) - else (incr token_number;next true) in + if growing then if bp >= pos then loc else (incr token_number;next true) + else if bp = pos then loc + else if bp > pos then (decr token_number;next false) + else (incr token_number;next true) in let loc = next (pos >= !last_pos) in - last_pos := pos; - let path = string_of_dirpath path in - let sc = match sc with Some sc -> " "^sc | None -> "" in - dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc) + last_pos := pos; + let path = string_of_dirpath path in + let sc = match sc with Some sc -> " "^sc | None -> "" in + dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc) (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -494,20 +494,20 @@ let find_constructor ref = try extended_locate qid with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in - match gref with - | SyntacticDef sp -> - let sdef = Syntax_def.search_syntactic_definition loc sp in - patt_of_rawterm loc sdef - | TrueGlobal r -> - let rec unf = function - | ConstRef cst -> - let v = Environ.constant_value (Global.env()) cst in - unf (global_of_constr v) - | ConstructRef c -> - if !dump then add_glob loc r; - c, [] - | _ -> raise Not_found - in unf r + match gref with + | SyntacticDef sp -> + let sdef = Syntax_def.search_syntactic_definition loc sp in + patt_of_rawterm loc sdef + | TrueGlobal r -> + let rec unf = function + | ConstRef cst -> + let v = Environ.constant_value (Global.env()) cst in + unf (global_of_constr v) + | ConstructRef c -> + if !dump then add_glob loc r; + c, [] + | _ -> raise Not_found + in unf r let find_pattern_variable = function | Ident (loc,id) -> id diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index cd013e559..c8756a49f 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -550,10 +550,10 @@ let func cs = Stream.from (fun i -> let (tok, loc) = next_token cs in - loct_add loct i loc; Some tok) + loct_add loct i loc; Some tok) in - current_location_table := loct; - (ts, loct_func loct) + current_location_table := loct; + (ts, loct_func loct) type location_table = (int * int) option array array ref let location_table () = !current_location_table diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index cb0d89143..94a70ccda 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -108,14 +108,16 @@ let add_compile verbose s = compile_list := (verbose,s) :: !compile_list let compile_files () = let init_state = States.freeze() in - List.iter - (fun (v,f) -> - States.unfreeze init_state; - if Options.do_translate () then - with_option translate_file (Vernac.compile v) f - else - Vernac.compile v f) - (List.rev !compile_list) + let coqdoc_init_state = Constrintern.coqdoc_freeze () in + List.iter + (fun (v,f) -> + States.unfreeze init_state; + Constrintern.coqdoc_unfreeze coqdoc_init_state; + if Options.do_translate () then + with_option translate_file (Vernac.compile v) f + else + Vernac.compile v f) + (List.rev !compile_list) let re_exec_version = ref "" let set_byte () = re_exec_version := "byte" diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d44227a80..f3bc0793f 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -126,27 +126,30 @@ let rec vernac_com interpfun (loc,com) = (* end translator state *) (* coqdoc state *) let cds = Constrintern.coqdoc_freeze() in - if !Options.translate_file then begin - let _,f = find_file_in_path (Library.get_load_paths ()) - (make_suffix fname ".v") in - chan_translate := open_out (f^"8"); - Pp.comments := [] - end; - begin try - read_vernac_file verbosely (make_suffix fname ".v"); - if !Options.translate_file then close_out !chan_translate; - chan_translate := ch; - Lexer.restore_com_state cs; - Pp.comments := cl; - Constrintern.coqdoc_unfreeze cds; - with e -> - if !Options.translate_file then close_out !chan_translate; - chan_translate := ch; - Lexer.restore_com_state cs; - Pp.comments := cl; - Constrintern.coqdoc_unfreeze cds; - raise e end; - + if !Options.translate_file then + begin + let _,f = find_file_in_path (Library.get_load_paths ()) + (make_suffix fname ".v") in + chan_translate := open_out (f^"8"); + Pp.comments := [] + end; + begin + try + read_vernac_file verbosely (make_suffix fname ".v"); + if !Options.translate_file then close_out !chan_translate; + chan_translate := ch; + Lexer.restore_com_state cs; + Pp.comments := cl; + Constrintern.coqdoc_unfreeze cds + with e -> + if !Options.translate_file then close_out !chan_translate; + chan_translate := ch; + Lexer.restore_com_state cs; + Pp.comments := cl; + Constrintern.coqdoc_unfreeze cds; + raise e + end + | VernacList l -> List.iter (fun (_,v) -> interp v) l | VernacTime v -> |