X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaScript.ml;h=9eb1dbf69c608c9ba231d4e46f45f3ae78fb1f18;hb=43ed97bb09bf148dfda74b3266b44143640b9643;hp=23de391c6ed37e486d1b0324f429325a41d98af4;hpb=afea2be14c1c197e0804e8607fc6dcc49ce46955;p=helm.git diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 23de391c6..9eb1dbf69 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -60,14 +60,6 @@ let first_line s = String.sub s 0 nl_pos with Not_found -> s - (** creates a statement AST for the Goal tactic, e.g. "goal 7" *) -let goal_ast n = - let module A = GrafiteAst in - let loc = HExtlib.dummy_floc in - A.Executable (loc, A.Tactical (loc, - A.Tactic (loc, A.Goal (loc, n)), - Some (A.Dot loc))) - type guistuff = { mathviewer:MatitaTypes.mathViewer; urichooser: UriManager.uri list -> UriManager.uri list; @@ -234,7 +226,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], "", parsed_text_length | TA.WHint (loc, term) -> - let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in + let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term, []),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in let entry = `Whelp (pp_macro mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; @@ -255,10 +247,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status | [uri] -> let suri = UriManager.string_of_uri uri in let ast loc = - TA.Executable (loc, (TA.Tactical (loc, - TA.Tactic (loc, - TA.Apply (loc, CicNotationPt.Uri (suri, None))), - Some (TA.Dot loc)))) in + TA.Executable (loc, (TA.Tactic (loc, + Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))), + TA.Dot loc))) in let text = comment parsed_text ^ "\n" ^ pp_eager_statement_ast (ast HExtlib.dummy_floc) in @@ -288,53 +279,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let t_and_ty = Cic.Cast (term,ty) in guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); [], "", parsed_text_length - | TA.Inline (_,suri) -> - let dbd = LibraryDb.instance () in - let uris = - let sql_pat = - (Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" suri) ^ "%" in - let query = - sprintf ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^ - "SELECT source FROM %s WHERE source LIKE \"%s\"") - (MetadataTypes.name_tbl ()) sql_pat - MetadataTypes.library_name_tbl sql_pat in - let result = HMysql.exec dbd query in - HMysql.map result - (function cols -> - match cols.(0) with - Some s -> UriManager.uri_of_string s - | _ -> assert false) - in -prerr_endline "Inizio sorting"; - let sorted_uris = MetadataDeps.topological_sort ~dbd uris in -prerr_endline "Fine sorting"; - let sorted_uris_without_xpointer = - HExtlib.filter_map - (function uri -> - let s = - Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:"" - (UriManager.string_of_uri uri) in - try - ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s); - None - with - Not_found -> - Some (UriManager.uri_of_string s) - ) sorted_uris - in - let declarative = - String.concat "\n\n" - (List.map - (fun uri -> -prerr_endline ("Stampo " ^ UriManager.string_of_uri uri); - try - ObjPp.obj_to_string 80 - (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) - with - _ (* BRRRRRRRRR *) -> "ERRORE IN STAMPA DI " ^ UriManager.string_of_uri uri - ) sorted_uris_without_xpointer) - in - [],declarative,String.length parsed_text + | TA.Inline (_,style,suri,prefix) -> + let str = ApplyTransformation.txt_of_inline_macro style suri prefix in + [], str, String.length parsed_text and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt @@ -363,6 +310,9 @@ script ex loc | `CANCEL -> raise MatitaTypes.Cancel) | _ -> () end; + ignore (buffer#move_mark (`NAME "beginning_of_statement") + ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars + (Glib.Utf8.length skipped_txt))) ; eval_with_engine guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt (TA.Executable (loc, ex)) @@ -501,6 +451,9 @@ object (self) (** text mark and tag representing locked part of a script *) val locked_mark = buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter + val beginning_of_statement_mark = + buffer#create_mark ~name:"beginning_of_statement" + ~left_gravity:true buffer#start_iter val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false] val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"] @@ -570,6 +523,7 @@ object (self) with | Margin -> self#notify | Not_found -> assert false + | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n" | exc -> self#notify; raise exc method retract () = @@ -587,6 +541,7 @@ object (self) self#notify with | Margin -> self#notify + | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n" | exc -> self#notify; raise exc method private getFuture = @@ -720,6 +675,7 @@ object (self) set_star (Filename.basename self#ppFilename) false method goto (pos: [`Top | `Bottom | `Cursor]) () = + try let old_locked_mark = `MARK (buffer#create_mark ~name:"old_locked_mark" @@ -799,7 +755,9 @@ object (self) | Margin -> dispose_remember (); dispose_old_locked_mark (); self#notify | exc -> dispose_remember (); dispose_old_locked_mark (); self#notify; raise exc) - + with Invalid_argument "Array.make" -> + HLog.error "The script is too big!\n" + method onGoingProof () = match self#grafite_status.proof_status with | No_proof | Proof _ -> false @@ -850,6 +808,7 @@ prerr_endline ("## " ^ string_of_int parsed_text_length); | HExtlib.Localized _ | CicNotationParser.Parse_error _ -> false | Margin | End_of_file -> true + | Invalid_argument "Array.make" -> false (* debug *) method dump () =