- if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
- let st =
- try
- GrafiteParser.parse_statement (Stream.of_string s)
- with
- CicNotationParser.Parse_error (floc,err) as exc ->
- 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
- raise (CicNotationParser.Parse_error (floc,err))
+ let module TAPp = GrafiteAstPp in
+ let module MD = GrafiteDisambiguator in
+ let module ML = MatitaMisc in
+ try
+ begin
+ match ex with
+ | TA.Command (_,TA.Set (_,"baseuri",u)) ->
+ if not (GrafiteMisc.is_empty u) then
+ (match
+ guistuff.ask_confirmation
+ ~title:"Baseuri redefinition"
+ ~message:(
+ "Baseuri " ^ u ^ " already exists.\n" ^
+ "Do you want to redefine the corresponding "^
+ "part of the library?")
+ with
+ | `YES ->
+ let basedir = Helm_registry.get "matita.basedir" in
+ LibraryClean.clean_baseuris ~basedir [u]
+ | `NO -> ()
+ | `CANCEL -> raise MatitaTypes.Cancel)
+ | _ -> ()
+ end;
+ eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text
+ (TA.Executable (loc, ex))
+ with
+ MatitaTypes.Cancel -> [], 0
+ | GrafiteEngine.Macro (_loc,lazy_macro) ->
+ let context =
+ match user_goal with
+ None -> []
+ | Some n -> GrafiteTypes.get_proof_context grafite_status n in
+ let grafite_status,macro = lazy_macro context in
+ eval_macro include_paths buffer guistuff lexicon_status grafite_status
+ user_goal unparsed_text parsed_text script macro
+
+and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
+ grafite_status user_goal script statement
+=
+ let (lexicon_status,st), unparsed_text =
+ match statement with
+ | `Raw text ->
+ if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
+ GrafiteParser.parse_statement (Ulexing.from_utf8_string text)
+ ~include_paths lexicon_status, text
+ | `Ast (st, text) -> (lexicon_status, st), text