diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide/coq_lex.mll | 20 | ||||
| -rw-r--r-- | ide/coqide/idetop.ml | 2 |
2 files changed, 17 insertions, 5 deletions
diff --git a/ide/coqide/coq_lex.mll b/ide/coqide/coq_lex.mll index fe9f108a94..a65954d566 100644 --- a/ide/coqide/coq_lex.mll +++ b/ide/coqide/coq_lex.mll @@ -50,7 +50,10 @@ and comment = parse | utf8_extra_byte { incr utf8_adjust; comment lexbuf } | _ { comment lexbuf } -and quotation o c n l = parse | eof { raise Unterminated } | _ { +and quotation o c n l = parse +| eof { raise Unterminated } +| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf } +| _ { let x = Lexing.lexeme lexbuf in if x = o then quotation_nesting o c n l 1 lexbuf else if x = c then @@ -59,7 +62,10 @@ and quotation o c n l = parse | eof { raise Unterminated } | _ { else quotation o c n l lexbuf } -and quotation_nesting o c n l v = parse | eof { raise Unterminated } | _ { +and quotation_nesting o c n l v = parse +| eof { raise Unterminated } +| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf } +| _ { let x = Lexing.lexeme lexbuf in if x = o then if n = v+1 then quotation o c n (l+1) lexbuf @@ -68,7 +74,10 @@ and quotation_nesting o c n l v = parse | eof { raise Unterminated } | _ { else quotation o c n l lexbuf } -and quotation_closing o c n l v = parse | eof { raise Unterminated } | _ { +and quotation_closing o c n l v = parse +| eof { raise Unterminated } +| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf } +| _ { let x = Lexing.lexeme lexbuf in if x = c then if n = v+1 then @@ -79,7 +88,10 @@ and quotation_closing o c n l v = parse | eof { raise Unterminated } | _ { else quotation o c n l lexbuf } -and quotation_start o c n = parse | eof { raise Unterminated } | _ { +and quotation_start o c n = parse +| eof { raise Unterminated } +| utf8_extra_byte { incr utf8_adjust; quotation o c n 1 lexbuf } +| _ { let x = Lexing.lexeme lexbuf in if x = o then quotation_start o c (n+1) lexbuf else quotation o c n 1 lexbuf diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index bd99cbed1b..2adc35ae3e 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -343,7 +343,7 @@ let search flags = let pstate = Vernacstate.Declare.get_pstate () in let sigma, env = match pstate with | None -> let env = Global.env () in Evd.(from_env env, env) - | Some p -> Declare.get_goal_context p 1 in + | Some p -> Declare.Proof.get_goal_context p 1 in List.map export_coq_object (Search.interface_search env sigma ( List.map (fun (c, b) -> (import_search_constraint c, b)) flags) ) |