X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=7569584274221cc125e438101f329c0da6265c9d;hb=34fad691712f60b4cd11510b9f73c09d25eaf125;hp=34e0408c598f281aa0d6bee4417bc3ad5493e407;hpb=82247d9af61693c803bbc87bc6df2de62f359976;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 34e0408c5..756958427 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -230,14 +230,13 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = let module CTC = CicTypeChecker in let module CU = CicUniv in (* no idea why ocaml wants this *) - let advance ?statement () = script#advance ?statement () in let parsed_text_length = String.length parsed_text in let dbd = MatitaDb.instance () in match mac with (* WHELP's stuff *) | TA.WMatch (loc, term) -> let term = disambiguate_macro_term term status user_goal in - let l = MQ.match_term ~dbd term in + let l = Whelp.match_term ~dbd term in let query_url = MatitaMisc.strip_suffix ~suffix:"." (HExtlib.trim_blanks unparsed_text) @@ -247,12 +246,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = [], parsed_text_length | TA.WInstance (loc, term) -> let term = disambiguate_macro_term term status user_goal in - let l = MQ.instance ~dbd term in + let l = Whelp.instance ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WLocate (loc, s) -> - let l = MQ.locate ~dbd s in + let l = Whelp.locate ~dbd s in let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length @@ -263,7 +262,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None | _ -> failwith "Not a MutInd" in - let l = MQ.elim ~dbd uri in + let l = Whelp.elim ~dbd uri in let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length @@ -347,7 +346,6 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script let module TAPp = GrafiteAstPp in let module MD = MatitaDisambiguator in let module ML = MatitacleanLib in - let parsed_text_length = String.length parsed_text in match ex with | TA.Command (loc, _) | TA.Tactical (loc, _, _) -> (try @@ -372,49 +370,18 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script | TA.Macro (_,mac) -> eval_macro guistuff status user_goal unparsed_text parsed_text script mac -let parse_statement baseoffset parsedlen ?error_tag (buffer: GText.buffer) text -= - try - GrafiteParser.parse_statement (Ulexing.from_utf8_string text) - with CicNotationParser.Parse_error (floc, err) as exn -> - match error_tag with - | None -> raise exn - | Some error_tag -> - let (x, y) = CicNotationPt.loc_of_floc floc in - let x = parsedlen + x in - let y = parsedlen + y in - let x' = baseoffset + x in - let y' = baseoffset + y in - let x_iter = buffer#get_iter (`OFFSET x') in - let y_iter = buffer#get_iter (`OFFSET y') in - buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter; - let id = ref None in - id := Some (buffer#connect#changed ~callback:(fun () -> - buffer#remove_tag error_tag ~start:buffer#start_iter - ~stop:buffer#end_iter; - match !id with - | None -> assert false (* a race condition occurred *) - | Some id -> - (new GObj.gobject_ops buffer#as_buffer)#disconnect id)); - let flocb,floce = floc in - let floc = - { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y } - in - buffer#place_cursor (buffer#get_iter (`OFFSET x')); - raise (CicNotationParser.Parse_error (floc, err)) - -let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer) - guistuff status user_goal script statement +let rec eval_statement (buffer : GText.buffer) guistuff status user_goal + script statement = let st, unparsed_text = match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; - parse_statement baseoffset parsedlen ~error_tag buffer text, text + GrafiteParser.parse_statement (Ulexing.from_utf8_string text), text | `Ast (st, text) -> st, text in let text_of_loc loc = - let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in + let parsed_text_length = snd (HExtlib.loc_of_floc loc) in let parsed_text = safe_substring unparsed_text 0 parsed_text_length in parsed_text, parsed_text_length in @@ -424,8 +391,16 @@ let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer) let remain_len = String.length unparsed_text - parsed_text_length in let s = String.sub unparsed_text parsed_text_length remain_len in let s,len = - eval_statement baseoffset (parsedlen + parsed_text_length) error_tag - buffer guistuff status user_goal script (`Raw s) + try + eval_statement buffer guistuff status user_goal script + (`Raw s) + with + HExtlib.Localized (floc, exn) -> + HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn + | MatitaDisambiguator.DisambiguationError (offset,errorll) -> + raise + (MatitaDisambiguator.DisambiguationError + (offset+parsed_text_length, errorll)) in (match s with | (status, (text, ast)) :: tl -> @@ -494,6 +469,7 @@ object (self) method locked_mark = locked_mark method locked_tag = locked_tag + method error_tag = error_tag (* history can't be empty, the invariant above grant that it contains at * least the init status *) @@ -501,10 +477,8 @@ object (self) method private _advance ?statement () = let rec aux st = - let baseoffset = (buffer#get_iter_at_mark (`MARK locked_mark))#offset in let (entries, parsed_len) = - eval_statement baseoffset 0 error_tag buffer guistuff self#status - userGoal self st + eval_statement buffer guistuff self#status userGoal self st in let (new_statuses, new_statements, new_asts) = let statuses, statements = List.split entries in @@ -534,7 +508,7 @@ object (self) in let text = self#getFuture in (try - (match parse_statement baseoffset 0 ?error_tag:None buffer text with + (match parse_statement baseoffset 0 buffer text with | TA.Executable (loc, TA.Tactical (_, tac, None)) as st when GrafiteAst.is_punctuation tac -> let len = snd (CicNotationPt.loc_of_floc loc) in @@ -774,7 +748,7 @@ object (self) let st = GrafiteParser.parse_statement (Ulexing.from_utf8_string s) in match st with | GrafiteAst.Comment (loc,_)-> - let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in + let parsed_text_length = snd (HExtlib.loc_of_floc loc) in let remain_len = String.length s - parsed_text_length in let next = String.sub s parsed_text_length remain_len in is_there_and_executable next