X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=c39e1de40a5ec9d9d7856718f196787ba9a4c1b3;hb=1aca50505c3ce6c76dd7d20d00e358707caffd4a;hp=552d4907a757c7727135ab38d796ee8a7981b571;hpb=d46411c038cccb932638fd9d131c5d858c80ac5e;p=helm.git diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 552d4907a..c39e1de40 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -26,7 +26,6 @@ (* $Id$ *) open Printf -open GrafiteTypes module TA = GrafiteAst @@ -65,14 +64,7 @@ let first_line s = String.sub s 0 nl_pos with Not_found -> s -type guistuff = { - mathviewer:MatitaTypes.mathViewer; - urichooser: UriManager.uri list -> UriManager.uri list; - ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; -} - -let eval_with_engine include_paths guistuff grafite_status user_goal - skipped_txt nonskipped_txt st +let eval_with_engine include_paths status skipped_txt nonskipped_txt st = let parsed_text_length = String.length skipped_txt + String.length nonskipped_txt @@ -80,9 +72,9 @@ let eval_with_engine include_paths guistuff grafite_status user_goal let text = skipped_txt ^ nonskipped_txt in let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in let enriched_history_fragment = - MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool + MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:(Helm_registry.get_bool "matita.do_heavy_checks") - grafite_status (text,prefix_len,st) + status (text,prefix_len,st) in let enriched_history_fragment = List.rev enriched_history_fragment in (* really fragile *) @@ -91,507 +83,116 @@ let eval_with_engine include_paths guistuff grafite_status user_goal (fun (acc, to_prepend) (status,alias) -> match alias with | None -> (status,to_prepend ^ nonskipped_txt)::acc,"" - | Some (k,value) -> - let newtxt = LexiconAstPp.pp_alias value in + | Some (_k,value) -> + let newtxt = GrafiteAstPp.pp_alias value in (status,to_prepend ^ newtxt ^ "\n")::acc, "") ([],skipped_txt) enriched_history_fragment in res,"",parsed_text_length ;; -(* this function calls the parser in a way that it does not perform inclusions, - * so that we can ensure the inclusion is performed after the included file - * is compiled (if needed). matitac does not need that, since it compiles files - * in the good order, here files may be compiled on demand. *) -let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statement) x = - try - f ~never_include:true ~include_paths x - with - | GrafiteParser.NoInclusionPerformed mafilename -> - let root, buri, _, tgt = - try Librarian.baseuri_of_script ~include_paths mafilename - with Librarian.NoRootFor _ -> - HLog.error ("The included file '"^mafilename^"' has no root file,"); - HLog.error "please create it."; - raise (Failure ("No root file for "^mafilename)) - in - let b = MatitacLib.Make.make root [tgt] in - if b then - try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ -> - raise - (Failure ("Including: "^tgt^ - "\nNothing to do... did you run matitadep?")) - else raise (Failure ("Compiling: " ^ tgt)) -;; +let pp_eager_statement_ast = GrafiteAstPp.pp_statement -let pp_eager_statement_ast = - GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) - -(* naive implementation of procedural proof script generation, - * starting from an applicatiove *auto generated) proof. - * this is out of place, but I like it :-P *) -let cic2grafite context menv t = - (* indents a proof script in a stupid way, better than nothing *) - let stupid_indenter s = - let next s = - let idx_square_o = try String.index s '[' with Not_found -> -1 in - let idx_square_c = try String.index s ']' with Not_found -> -1 in - let idx_pipe = try String.index s '|' with Not_found -> -1 in - let tok = - List.sort (fun (i,_) (j,_) -> compare i j) - [idx_square_o,'[';idx_square_c,']';idx_pipe,'|'] - in - let tok = List.filter (fun (i,_) -> i <> -1) tok in - match tok with - | (i,c)::_ -> Some (i,c) - | _ -> None - in - let break_apply n s = - let tab = String.make (n+1) ' ' in - Pcre.replace ~templ:(".\n" ^ tab ^ "apply") ~pat:"\\.apply" s - in - let rec ind n s = - match next s with - | None -> - s - | Some (position, char) -> - try - let s1, s2 = - String.sub s 0 position, - String.sub s (position+1) (String.length s - (position+1)) - in - match char with - | '[' -> break_apply n s1 ^ "\n" ^ String.make (n+2) ' ' ^ - "[" ^ ind (n+2) s2 - | '|' -> break_apply n s1 ^ "\n" ^ String.make n ' ' ^ - "|" ^ ind n s2 - | ']' -> break_apply n s1 ^ "\n" ^ String.make n ' ' ^ - "]" ^ ind (n-2) s2 - | _ -> assert false - with - Invalid_argument err -> - prerr_endline err; - s - in - ind 0 s - in - let module PT = CicNotationPt in - let module GA = GrafiteAst in - let pp_t context t = - let names = - List.map (function Some (n,_) -> Some n | None -> None) context - in - CicPp.pp t names - in - let sort_of context t = - try - let ty,_ = - CicTypeChecker.type_of_aux' menv context t - CicUniv.oblivion_ugraph - in - let sort,_ = CicTypeChecker.type_of_aux' menv context ty - CicUniv.oblivion_ugraph - in - match sort with - | Cic.Sort Cic.Prop -> true - | _ -> false - with - CicTypeChecker.TypeCheckerFailure _ -> - HLog.error "auto proof to sript transformation error"; false - in - let floc = HExtlib.dummy_floc in - (* minimalisti cic.term -> pt.term *) - let print_term c t = - let rec aux c = function - | Cic.Rel _ - | Cic.MutConstruct _ - | Cic.MutInd _ - | Cic.Const _ as t -> - PT.Ident (pp_t c t, None) - | Cic.Appl l -> PT.Appl (List.map (aux c) l) - | Cic.Implicit _ -> PT.Implicit `JustOne - | Cic.Lambda (Cic.Name n, s, t) -> - PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)), - aux (Some (Cic.Name n, Cic.Decl s)::c) t) - | Cic.Prod (Cic.Name n, s, t) -> - PT.Binder (`Forall, (PT.Ident (n,None), Some (aux c s)), - aux (Some (Cic.Name n, Cic.Decl s)::c) t) - | Cic.LetIn (Cic.Name n, s, ty, t) -> - PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)), - aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t) - | Cic.Meta _ -> PT.Implicit `JustOne - | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u) - | Cic.Sort Cic.Set -> PT.Sort `Set - | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u) - | Cic.Sort Cic.Prop -> PT.Sort `Prop - | _ as t -> PT.Ident ("ERROR: "^CicPp.ppterm t, None) - in - aux c t - in - (* prints an applicative proof, that is an auto proof. - * don't use in the general case! *) - let rec print_proof context = function - | Cic.Rel _ - | Cic.Const _ as t -> - [GA.Executable (floc, - GA.Tactic (floc, - Some (GA.Apply (floc, print_term context t)), GA.Dot floc))] - | Cic.Appl (he::tl) -> - let tl = List.map (fun t -> t, sort_of context t) tl in - let subgoals = - HExtlib.filter_map (function (t,true) -> Some t | _ -> None) tl - in - let args = - List.map (function | (t,true) -> Cic.Implicit None | (t,_) -> t) tl - in - if List.length subgoals > 1 then - (* branch *) - [GA.Executable (floc, - GA.Tactic (floc, - Some (GA.Apply (floc, print_term context (Cic.Appl (he::args)))), - GA.Semicolon floc))] @ - [GA.Executable (floc, GA.Tactic (floc, None, GA.Branch floc))] @ - (HExtlib.list_concat - ~sep:[GA.Executable (floc, GA.Tactic (floc, None,GA.Shift floc))] - (List.map (print_proof context) subgoals)) @ - [GA.Executable (floc, GA.Tactic (floc, None,GA.Merge floc))] - else - (* simple apply *) - [GA.Executable (floc, - GA.Tactic (floc, - Some (GA.Apply - (floc, print_term context (Cic.Appl (he::args)) )), GA.Dot floc))] - @ - (match subgoals with - | [] -> [] - | [x] -> print_proof context x - | _ -> assert false) - | Cic.Lambda (Cic.Name n, ty, bo) -> - [GA.Executable (floc, - GA.Tactic (floc, - Some (GA.Cut (floc, Some n, (print_term context ty))), - GA.Branch floc))] @ - (print_proof (Some (Cic.Name n, Cic.Decl ty)::context) bo) @ - [GA.Executable (floc, GA.Tactic (floc, None,GA.Shift floc))] @ - [GA.Executable (floc, GA.Tactic (floc, - Some (GA.Assumption floc),GA.Merge floc))] - | _ -> [] - (* - debug_print (lazy (CicPp.ppterm t)); - assert false - *) - in - (* performs a lambda closure of the proof term abstracting metas. - * this is really an approximation of a closure, local subst of metas - * is not kept into account *) - let close_pt menv context t = - let metas = CicUtil.metas_of_term t in - let metas = - HExtlib.list_uniq ~eq:(fun (i,_) (j,_) -> i = j) - (List.sort (fun (i,_) (j,_) -> compare i j) metas) - in - let mk_rels_and_collapse_metas metas = - let rec aux i map acc acc1 = function - | [] -> acc, acc1, map - | (j,_ as m)::tl -> - let _,_,ty = CicUtil.lookup_meta j menv in - try - let n = List.assoc ty map in - aux i map (Cic.Rel n :: acc) (m::acc1) tl - with Not_found -> - let map = (ty, i)::map in - aux (i+1) map (Cic.Rel i :: acc) (m::acc1) tl - in - aux 1 [] [] [] metas - in - let rels, metas, map = mk_rels_and_collapse_metas metas in - let n_lambdas = List.length map in - let t = - if metas = [] then - t - else - let t = - ProofEngineReduction.replace_lifting - ~what:(List.map (fun (x,_) -> Cic.Meta (x,[])) metas) - ~with_what:rels - ~context:context - ~equality:(fun _ x y -> - match x,y with - | Cic.Meta(i,_), Cic.Meta(j,_) when i=j -> true - | _ -> false) - ~where:(CicSubstitution.lift n_lambdas t) - in - let rec mk_lam = function - | [] -> t - | (ty,n)::tl -> - let name = "fresh_"^ string_of_int n in - Cic.Lambda (Cic.Name name, ty, mk_lam tl) - in - mk_lam - (fst (List.fold_left - (fun (l,liftno) (ty,_) -> - (l @ [CicSubstitution.lift liftno ty,liftno] , liftno+1)) - ([],0) map)) - in - t - in - let ast = print_proof context (close_pt menv context t) in - let pp t = - (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string - * which will show up using the following command line: - * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *) - let width = max_int in - let term_pp content_term = - let pres_term = TermContentPres.pp_ast content_term in - let lookup_uri = fun _ -> None in - let markup = CicNotationPres.render ~lookup_uri pres_term in - let s = "(" ^ BoxPp.render_to_string - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - List.hd width markup ^ ")" in - Pcre.substitute - ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s - in - CicNotationPp.set_pp_term term_pp; - let lazy_term_pp = fun x -> assert false in - let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in - GrafiteAstPp.pp_statement - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - ~term_pp ~lazy_term_pp ~obj_pp t - in - let script = String.concat "" (List.map pp ast) in - prerr_endline script; - stupid_indenter script -;; -let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = +let eval_nmacro _include_paths (_buffer : GText.buffer) status _unparsed_text parsed_text script mac = let parsed_text_length = String.length parsed_text in match mac with | TA.Screenshot (_,name) -> - let status = script#grafite_status in + let status = script#status in let _,_,menv,subst,_ = status#obj in let name = Filename.dirname (script#filename) ^ "/" ^ name in let sequents = let selected = Continuationals.Stack.head_goals status#stack in List.filter (fun x,_ -> List.mem x selected) menv in - guistuff.mathviewer#screenshot status sequents menv subst name; + CicMathView.screenshot status sequents menv subst name; [status, parsed_text], "", parsed_text_length | TA.NCheck (_,t) -> - let status = script#grafite_status in + let status = script#status in let _,_,menv,subst,_ = status#obj in let ctx = - try let _,(_,ctx,_) = List.hd menv in ctx - with Failure "hd" -> [] + match Continuationals.Stack.head_goals status#stack with + [] -> [] + | g::tl -> + if tl <> [] then + HLog.warn + "Many goals focused. Using the context of the first one\n"; + let ctx = try + let _, ctx, _ = NCicUtils.lookup_meta g menv in ctx + with NCicUtils.Meta_not_found _ -> + HLog.warn "Current goal is closed. Using empty context."; + [ ] + in ctx in let m, s, status, t = GrafiteDisambiguate.disambiguate_nterm - None status ctx menv subst (parsed_text,parsed_text_length, - CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne)) + status `XTNone ctx menv subst (parsed_text,parsed_text_length, + NotationPt.Cast (t,NotationPt.Implicit `JustOne)) (* XXX use the metasenv, if possible *) in - guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s)); + MatitaMathView.cicBrowser (Some (`NCic (t,ctx,m,s))); [status, parsed_text], "", parsed_text_length | TA.NIntroGuess _loc -> let names_ref = ref [] in - let s = - NTactics.intros_tac ~names_ref [] script#grafite_status - in + let s = NTactics.intros_tac ~names_ref [] script#status in let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in - [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length + [s, nl ^ "#" ^ String.concat " #" !names_ref], "", parsed_text_length | TA.NAutoInteractive (_loc, (None,a)) -> let trace_ref = ref [] in - let s = - NnAuto.auto_tac - ~params:(None,a) ~trace_ref script#grafite_status - in + let s = NnAuto.auto_tac ~params:(None,a) ~trace_ref script#status in let depth = try List.assoc "depth" a with Not_found -> "" in - let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in + let width = + try List.assoc "width" a + with Not_found -> "" + in + let trace = "/"^(if int_of_string depth > 1 then depth ^ " width=" ^ width else "")^" by " in let thms = match !trace_ref with - | [] -> "{}" + | [] -> "" | thms -> String.concat ", " (HExtlib.filter_map (function - | CicNotationPt.NRef r -> Some (NCicPp.r2s true r) + | NotationPt.NRef r -> Some (NCicPp.r2s status true r) | _ -> None) thms) in let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in - [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length + [s, nl ^ trace ^ thms ^ "/"], "", parsed_text_length | TA.NAutoInteractive (_, (Some _,_)) -> assert false -let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = - let module MQ = MetadataQuery in - let module CTC = CicTypeChecker in - (* no idea why ocaml wants this *) - let parsed_text_length = String.length parsed_text in - let dbd = LibraryDb.instance () in - match mac with - (* REAL macro *) - | TA.Hint (loc, rewrite) -> (* MATITA 1.0 *) assert false - | TA.Eval (_, kind, term) -> - let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in - let context = - match user_goal with - None -> [] - | Some n -> GrafiteTypes.get_proof_context grafite_status n in - let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in - let term = - match kind with - | `Normalize -> - CicReduction.normalize ~delta:true ~subst:[] context term - | `Simpl -> - ProofEngineReduction.simpl context term - | `Unfold None -> - ProofEngineReduction.unfold ?what:None context term - | `Unfold (Some lazy_term) -> - let what, _, _ = - lazy_term context metasenv CicUniv.empty_ugraph in - ProofEngineReduction.unfold ~what context term - | `Whd -> - CicReduction.whd ~delta:true ~subst:[] context term - in - let t_and_ty = Cic.Cast (term,ty) in - guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); - [(grafite_status#set_proof_status No_proof), parsed_text ],"", - parsed_text_length - | TA.Check (_,term) -> - let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in - let context = - match user_goal with - None -> [] - | Some n -> GrafiteTypes.get_proof_context grafite_status n in - let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in - let t_and_ty = Cic.Cast (term,ty) in - guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); - [], "", parsed_text_length - | TA.AutoInteractive (_, params) -> - let user_goal' = - match user_goal with - Some n -> n - | None -> raise NoUnfinishedProof - in - let proof = GrafiteTypes.get_current_proof grafite_status in - let proof_status = proof,user_goal' in - (try - let _,menv,_,_,_,_ = proof in - let i,cc,ty = CicUtil.lookup_meta user_goal' menv in - let timestamp = Unix.gettimeofday () in - let (_,menv,subst,_,_,_), _ = - ProofEngineTypes.apply_tactic - (Auto.auto_tac ~dbd ~params - ~automation_cache:grafite_status#automation_cache) - proof_status - in - let proof_term = - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable cc - in - CicMetaSubst.apply_subst subst (Cic.Meta (i,irl)) - in - let time = Unix.gettimeofday () -. timestamp in - let size, depth = Auto.size_and_depth cc menv proof_term in - let trailer = - Printf.sprintf - "\n(* end auto(%s) proof: TIME=%4.2f SIZE=%d DEPTH=%d *)" - Auto.revision time size depth - in - let proof_script = - if List.exists (fun (s,_) -> s = "paramodulation") (snd params) then - let proof_term, how_many_lambdas = - Auto.lambda_close ~prefix_name:"orrible_hack_" - proof_term menv cc - in - let ty,_ = - CicTypeChecker.type_of_aux' - [] [] proof_term CicUniv.empty_ugraph - in - prerr_endline (CicPp.ppterm proof_term ^ " n lambda= " ^ string_of_int how_many_lambdas); - (* use declarative output *) - let obj = - (* il proof_term vive in cc, devo metterci i lambda no? *) - (Cic.CurrentProof ("xxx",[],proof_term,ty,[],[])) - in - ApplyTransformation.txt_of_cic_object - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - ~skip_thm_and_qed:true - ~skip_initial_lambdas:how_many_lambdas - 80 [] obj - else - if true then - (* use cic2grafite *) - cic2grafite cc menv proof_term - else - (* alternative using FG stuff *) - let map_unicode_to_tex = - Helm_registry.get_bool "matita.paste_unicode_as_tex" - in - ApplyTransformation.procedural_txt_of_cic_term - ~map_unicode_to_tex 78 [] cc proof_term - in - let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in - [],text,parsed_text_length - with - ProofEngineTypes.Fail _ as exn -> - raise exn - (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *)) - | TA.Inline (_, suri, params) -> - let str = "\n\n" ^ - ApplyTransformation.txt_of_inline_macro - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - params suri - in - [], str, String.length parsed_text - -and eval_executable include_paths (buffer : GText.buffer) guistuff -grafite_status user_goal unparsed_text skipped_txt nonskipped_txt -script ex loc +let rec eval_executable include_paths (buffer : GText.buffer) +status unparsed_text skipped_txt nonskipped_txt script ex loc = try 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 include_paths - guistuff grafite_status user_goal skipped_txt nonskipped_txt - (TA.Executable (loc, ex)) + eval_with_engine include_paths status skipped_txt nonskipped_txt + (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 grafite_status - user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro | GrafiteEngine.NMacro (_loc,macro) -> - eval_nmacro include_paths buffer guistuff grafite_status - user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro + eval_nmacro include_paths buffer status + unparsed_text (skipped_txt ^ nonskipped_txt) script macro -and eval_statement include_paths (buffer : GText.buffer) guistuff - grafite_status user_goal script statement +and eval_statement include_paths (buffer : GText.buffer) status script + statement = - let (grafite_status,st), unparsed_text = + let st,unparsed_text = match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; - let ast = - wrap_with_make include_paths - (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) - grafite_status - in - ast, text - | `Ast (st, text) -> (grafite_status, st), text + let strm = + GrafiteParser.parsable_statement status + (Ulexing.from_utf8_string text) in + let ast = MatitaEngine.get_ast status include_paths strm in + ast, text + | `Ast (st, text) -> st, text in let text_of_loc floc = let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in @@ -603,27 +204,22 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff txt,nonskipped_txt,skipped_txt,len in match st with - | GrafiteParser.LNone loc -> - let parsed_text, _, _, parsed_text_length = text_of_loc loc in - [grafite_status,parsed_text],"", - parsed_text_length - | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> - let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in - eval_executable include_paths buffer guistuff - grafite_status user_goal unparsed_text skipped nonskipped script ex loc - | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))) + | GrafiteAst.Executable (loc, ex) -> + let _, nonskipped, skipped, _parsed_text_length = text_of_loc loc in + eval_executable include_paths buffer status unparsed_text + skipped nonskipped script ex loc + | GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex)) when Helm_registry.get_bool "matita.execcomments" -> - let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in - eval_executable include_paths buffer guistuff - grafite_status user_goal unparsed_text skipped nonskipped script ex loc - | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> + let _, nonskipped, skipped, _parsed_text_length = text_of_loc loc in + eval_executable include_paths buffer status unparsed_text + skipped nonskipped script ex loc + | GrafiteAst.Comment (loc, _) -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in 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,text,len = try - eval_statement include_paths buffer guistuff - grafite_status user_goal script (`Raw s) + eval_statement include_paths buffer status script (`Raw s) with HExtlib.Localized (floc, exn) -> HExtlib.raise_localized_exception @@ -643,58 +239,62 @@ let fresh_script_id = let i = ref 0 in fun () -> incr i; !i -class script ~(source_view: GSourceView2.source_view) - ~(mathviewer: MatitaTypes.mathViewer) - ~set_star - ~ask_confirmation - ~urichooser - () = +(** Selection handling + * Two clipboards are used: "clipboard" and "primary". + * "primary" is used by X, when you hit the middle button mouse is content is + * pasted between applications. In Matita this selection always contain the + * textual version of the selected term. + * "clipboard" is used inside Matita only and support ATM two different targets: + * "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may + * be added + *) +class script ~(parent:GBin.scrolled_window) ~tab_label () = +let source_view = + GSourceView3.source_view + ~auto_indent:true + ~insert_spaces_instead_of_tabs:true ~tab_width:2 + ~right_margin_position:80 ~show_right_margin:true + ~smart_home_end:`AFTER + ~packing:parent#add + () in let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in +let _ = + source_buffer#connect#notify_can_undo + ~callback:(MatitaMisc.get_gui ())#main#undoMenuItem#misc#set_sensitive in +let _ = + source_buffer#connect#notify_can_redo + ~callback:(MatitaMisc.get_gui ())#main#redoMenuItem#misc#set_sensitive in +let similarsymbols_tag_name = "similarsymbolos" in +let similarsymbols_tag = `NAME similarsymbols_tag_name in let initial_statuses current baseuri = - let empty_lstatus = new LexiconEngine.status in + let status = new MatitaEngine.status baseuri in (match current with - Some current -> - LexiconSync.time_travel ~present:current ~past:empty_lstatus; - GrafiteSync.time_travel ~present:current (); - (* CSC: there is a known bug in invalidation; temporary fix here *) - NCicEnvironment.invalidate () + Some _current -> NCicLibrary.time_travel status; +(* + (* MATITA 1.0: there is a known bug in invalidation; temporary fix here *) + NCicEnvironment.invalidate () *) | None -> ()); - let lexicon_status = - CicNotation2.load_notation ~include_paths:[] empty_lstatus - BuildTimeConf.core_notation_script - in - let grafite_status = GrafiteSync.init lexicon_status baseuri in - grafite_status -in -let read_include_paths file = - try - let root, _buri, _fname, _tgt = - Librarian.baseuri_of_script ~include_paths:[] file - in - let rc = - Str.split (Str.regexp " ") - (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) - in - List.iter (HLog.debug) rc; rc - with Librarian.NoRootFor _ | Not_found -> [] + status in let default_buri = "cic:/matita/tests" in let default_fname = ".unnamed.ma" in object (self) val mutable include_paths_ = [] + val clipboard = GData.clipboard Gdk.Atom.clipboard + (*val primary = GData.clipboard Gdk.Atom.primary*) + val mutable similarsymbols = [] + val mutable similarsymbols_orig = [] + val similar_memory = Hashtbl.create 97 + val mutable old_used_memory = false val scriptId = fresh_script_id () - val guistuff = { - mathviewer = mathviewer; - urichooser = urichooser; - ask_confirmation = ask_confirmation; - } - val mutable filename_ = (None : string option) method has_name = filename_ <> None + + method source_view = source_view method include_paths = include_paths_ @ @@ -703,7 +303,7 @@ object (self) method private curdir = try let root, _buri, _fname, _tgt = - Librarian.baseuri_of_script ~include_paths:self#include_paths + Librarian.baseuri_of_script ~include_paths:self#include_paths self#filename in root @@ -718,15 +318,107 @@ object (self) Librarian.baseuri_of_script ~include_paths:self#include_paths f in buri - with Librarian.NoRootFor _ -> default_buri + with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> default_buri method filename = match filename_ with None -> default_fname | Some f -> f initializer + ignore + (source_view#source_buffer#begin_not_undoable_action (); + self#reset (); + self#template (); + source_view#source_buffer#end_not_undoable_action ()); + MatitaMisc.observe_font_size (fun font_size -> + source_view#misc#modify_font_by_name + (sprintf "%s %d" BuildTimeConf.script_font font_size)); + source_view#misc#grab_focus (); + ignore(source_view#source_buffer#set_language + (Some MatitaGtkMisc.matita_lang)); + ignore(source_view#source_buffer#set_highlight_syntax true); + ignore(source_view#connect#after#paste_clipboard + ~callback:(fun () -> self#clean_dirty_lock)); ignore (GMain.Timeout.add ~ms:300000 ~callback:(fun _ -> self#_saveToBackupFile ();true)); ignore (buffer#connect#modified_changed - (fun _ -> set_star buffer#modified)) + (fun _ -> self#set_star buffer#modified)); + (* clean_locked is set to true only "during" a PRIMARY paste + operation (i.e. by clicking with the second mouse button) *) + let clean_locked = ref false in + ignore(source_view#event#connect#button_press + ~callback: + (fun button -> + if GdkEvent.Button.button button = 2 then + clean_locked := true; + false + )); + ignore(source_view#event#connect#button_release + ~callback:(fun _button -> clean_locked := false; false)); + ignore(source_view#buffer#connect#after#apply_tag + ~callback:( + fun tag ~start:_ ~stop:_ -> + if !clean_locked && + tag#get_oid = self#locked_tag#get_oid + then + begin + clean_locked := false; + self#clean_dirty_lock; + clean_locked := true + end)); + ignore(source_view#source_buffer#connect#after#insert_text + ~callback:(fun iter str -> + if (MatitaMisc.get_gui ())#main#menuitemAutoAltL#active && (str = " " || str = "\n") then + ignore(self#expand_virtual_if_any iter str))); + ignore(source_view#connect#after#populate_popup + ~callback:(fun pre_menu -> + let menu = new GMenu.menu pre_menu in + let menuItems = menu#children in + let undoMenuItem, redoMenuItem = + match menuItems with + [undo;redo;_sep1;cut;copy;paste;delete;_sep2; + _selectall;_sep3;_inputmethod;_insertunicodecharacter] -> + List.iter menu#remove [ copy; cut; delete; paste ]; + undo,redo + | _ -> assert false in + let add_menu_item = + let i = ref 2 in (* last occupied position *) + fun ~label -> + incr i; + GMenu.menu_item ~label ~packing:(menu#insert ~pos:!i) () in + let copy = add_menu_item ~label:"Copy" in + let cut = add_menu_item ~label:"Cut" in + let delete = add_menu_item ~label:"Delete" in + let paste = add_menu_item ~label:"Paste" in + let paste_pattern = add_menu_item ~label:"Paste as pattern" in + copy#misc#set_sensitive self#canCopy; + cut#misc#set_sensitive self#canCut; + delete#misc#set_sensitive self#canDelete; + paste#misc#set_sensitive self#canPaste; + paste_pattern#misc#set_sensitive self#canPastePattern; + MatitaGtkMisc.connect_menu_item copy self#copy; + MatitaGtkMisc.connect_menu_item cut self#cut; + MatitaGtkMisc.connect_menu_item delete self#delete; + MatitaGtkMisc.connect_menu_item paste self#paste; + MatitaGtkMisc.connect_menu_item paste_pattern self#pastePattern; + let new_undoMenuItem = + GMenu.menu_item + ~use_mnemonic:true + ~label:"_Undo" + ~packing:(menu#insert ~pos:0) () in + new_undoMenuItem#misc#set_sensitive + undoMenuItem#misc#sensitive; + menu#remove (undoMenuItem :> GMenu.menu_item); + MatitaGtkMisc.connect_menu_item new_undoMenuItem + (fun () -> self#safe_undo); + let new_redoMenuItem = + GMenu.menu_item + ~use_mnemonic:true + ~label:"_Redo" + ~packing:(menu#insert ~pos:1) () in + new_redoMenuItem#misc#set_sensitive + redoMenuItem#misc#sensitive; + menu#remove (redoMenuItem :> GMenu.menu_item); + MatitaGtkMisc.connect_menu_item new_redoMenuItem + (fun () -> self#safe_redo))); val mutable statements = [] (** executed statements *) @@ -736,9 +428,6 @@ object (self) * the script. * Invariant: this list length is 1 + length of statements *) - (** goal as seen by the user (i.e. metano corresponding to current tab) *) - val mutable userGoal = None - (** text mark and tag representing locked part of a script *) val locked_mark = buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter @@ -748,13 +437,223 @@ object (self) val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false] val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"] + (** unicode handling *) + method nextSimilarSymbol = + let write_similarsymbol s = + let s = Glib.Utf8.from_unichar s in + let iter = source_view#source_buffer#get_iter_at_mark `INSERT in + assert(Glib.Utf8.validate s); + source_view#source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars 1); + source_view#source_buffer#insert ~iter:(source_view#source_buffer#get_iter_at_mark `INSERT) s; + (try source_view#source_buffer#delete_mark similarsymbols_tag + with GText.No_such_mark _ -> ()); + ignore(source_view#source_buffer#create_mark ~name:similarsymbols_tag_name + (source_view#source_buffer#get_iter_at_mark `INSERT)); + in + let new_similarsymbol = + try + let iter_ins = source_view#source_buffer#get_iter_at_mark `INSERT in + let iter_lig = source_view#source_buffer#get_iter_at_mark similarsymbols_tag in + not (iter_ins#equal iter_lig) + with GText.No_such_mark _ -> true + in + if new_similarsymbol then + (if not(self#expand_virtual_if_any (source_view#source_buffer#get_iter_at_mark `INSERT) "")then + let last_symbol = + let i = source_view#source_buffer#get_iter_at_mark `INSERT in + Glib.Utf8.first_char (i#get_slice ~stop:(i#copy#backward_chars 1)) + in + (match Virtuals.similar_symbols last_symbol with + | [] -> () + | eqclass -> + similarsymbols_orig <- eqclass; + let is_used = + try Hashtbl.find similar_memory similarsymbols_orig + with Not_found -> + let is_used = List.map (fun x -> x,false) eqclass in + Hashtbl.add similar_memory eqclass is_used; + is_used + in + let hd, next, tl = + let used, unused = + List.partition (fun s -> List.assoc s is_used) eqclass + in + match used @ unused with a::b::c -> a,b,c | _ -> assert false + in + let hd, tl = + if hd = last_symbol then next, tl @ [hd] else hd, (next::tl) + in + old_used_memory <- List.assoc hd is_used; + let is_used = + (hd,true) :: List.filter (fun (x,_) -> x <> hd) is_used + in + Hashtbl.replace similar_memory similarsymbols_orig is_used; + write_similarsymbol hd; + similarsymbols <- tl @ [ hd ])) + else + match similarsymbols with + | [] -> () + | hd :: tl -> + let is_used = Hashtbl.find similar_memory similarsymbols_orig in + let last = HExtlib.list_last tl in + let old_used_for_last = old_used_memory in + old_used_memory <- List.assoc hd is_used; + let is_used = + (hd, true) :: (last,old_used_for_last) :: + List.filter (fun (x,_) -> x <> last && x <> hd) is_used + in + Hashtbl.replace similar_memory similarsymbols_orig is_used; + similarsymbols <- tl @ [ hd ]; + write_similarsymbol hd + + method private reset_similarsymbols = + similarsymbols <- []; + similarsymbols_orig <- []; + try source_view#source_buffer#delete_mark similarsymbols_tag + with GText.No_such_mark _ -> () + + method private expand_virtual_if_any iter tok = + try + let len = MatitaGtkMisc.utf8_string_length tok in + let last_word = + let prev = iter#copy#backward_chars len in + prev#get_slice ~stop:(prev#copy#backward_find_char + (fun x -> Glib.Unichar.isspace x || x = Glib.Utf8.first_char "\\")) + in + let inplaceof, symb = Virtuals.symbol_of_virtual last_word in + self#reset_similarsymbols; + let s = Glib.Utf8.from_unichar symb in + assert(Glib.Utf8.validate s); + source_view#source_buffer#delete ~start:iter + ~stop:(iter#copy#backward_chars + (MatitaGtkMisc.utf8_string_length inplaceof + len)); + source_view#source_buffer#insert ~iter + (if inplaceof.[0] = '\\' then s else (s ^ tok)); + true + with Virtuals.Not_a_virtual -> false + + (** selections / clipboards handling *) + + method markupSelected = MatitaMathView.has_selection () + method private textSelected = + (source_view#source_buffer#get_iter_at_mark `INSERT)#compare + (source_view#source_buffer#get_iter_at_mark `SEL_BOUND) <> 0 + method private markupStored = MatitaMathView.has_clipboard () + method private textStored = clipboard#text <> None + method canCopy = self#textSelected + method canCut = self#textSelected + method canDelete = self#textSelected + (*CSC: WRONG CODE: we should look in the clipboard instead! *) + method canPaste = self#markupStored || self#textStored + method canPastePattern = self#markupStored + + method safe_undo = + (* phase 1: we save the actual status of the marks and we undo *) + let locked_mark = `MARK (self#locked_mark) in + let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in + let locked_iter_offset = locked_iter#offset in + let mark2 = + `MARK + (source_view#buffer#create_mark ~name:"lock_point" + ~left_gravity:true locked_iter) in + source_view#source_buffer#undo (); + (* phase 2: we save the cursor position and we redo, restoring + the previous status of all the marks *) + let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in + let mark = + `MARK + (source_view#buffer#create_mark ~name:"undo_point" + ~left_gravity:true cursor_iter) + in + source_view#source_buffer#redo (); + let mark_iter = source_view#buffer#get_iter_at_mark mark in + let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in + let mark2_iter = mark2_iter#set_offset locked_iter_offset in + source_view#buffer#move_mark locked_mark ~where:mark2_iter; + source_view#buffer#delete_mark mark; + source_view#buffer#delete_mark mark2; + (* phase 3: if after the undo the cursor was in the locked area, + then we move it there again and we perform a goto *) + if mark_iter#offset < locked_iter_offset then + begin + source_view#buffer#move_mark `INSERT ~where:mark_iter; + self#goto `Cursor (); + end; + (* phase 4: we perform again the undo. This time we are sure that + the text to undo is not locked *) + source_view#source_buffer#undo (); + source_view#misc#grab_focus () + + method safe_redo = + (* phase 1: we save the actual status of the marks, we redo and + we undo *) + let locked_mark = `MARK (self#locked_mark) in + let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in + let locked_iter_offset = locked_iter#offset in + let mark2 = + `MARK + (source_view#buffer#create_mark ~name:"lock_point" + ~left_gravity:true locked_iter) in + source_view#source_buffer#redo (); + source_view#source_buffer#undo (); + (* phase 2: we save the cursor position and we restore + the previous status of all the marks *) + let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in + let mark = + `MARK + (source_view#buffer#create_mark ~name:"undo_point" + ~left_gravity:true cursor_iter) + in + let mark_iter = source_view#buffer#get_iter_at_mark mark in + let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in + let mark2_iter = mark2_iter#set_offset locked_iter_offset in + source_view#buffer#move_mark locked_mark ~where:mark2_iter; + source_view#buffer#delete_mark mark; + source_view#buffer#delete_mark mark2; + (* phase 3: if after the undo the cursor is in the locked area, + then we move it there again and we perform a goto *) + if mark_iter#offset < locked_iter_offset then + begin + source_view#buffer#move_mark `INSERT ~where:mark_iter; + self#goto `Cursor (); + end; + (* phase 4: we perform again the redo. This time we are sure that + the text to redo is not locked *) + source_view#source_buffer#redo (); + source_view#misc#grab_focus () + + + method copy () = + if self#textSelected + then begin + MatitaMathView.empty_clipboard (); + source_view#buffer#copy_clipboard clipboard; + end else + MatitaMathView.copy_selection () + + method cut () = + source_view#buffer#cut_clipboard clipboard; + MatitaMathView.empty_clipboard () + + method delete () = + ignore (source_view#buffer#delete_selection ()) + + method paste () = + if MatitaMathView.has_clipboard () + then source_view#buffer#insert (MatitaMathView.paste_clipboard `Term) + else source_view#buffer#paste_clipboard clipboard; + self#clean_dirty_lock + + method pastePattern () = + source_view#buffer#insert (MatitaMathView.paste_clipboard `Pattern) + 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 grafite_status *) - method grafite_status = match history with s::_ -> s | _ -> assert false + method status = match history with s::_ -> s | _ -> assert false method private _advance ?statement () = let s = match statement with Some s -> s | None -> self#getFuture in @@ -763,8 +662,7 @@ object (self) let time1 = Unix.gettimeofday () in let entries, newtext, parsed_len = try - eval_statement self#include_paths buffer guistuff - self#grafite_status userGoal self (`Raw s) + eval_statement self#include_paths buffer self#status self (`Raw s) with End_of_file -> raise Margin in let time2 = Unix.gettimeofday () in @@ -788,24 +686,10 @@ object (self) end; end; self#moveMark (Glib.Utf8.length new_text); - buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext; - (* here we need to set the Goal in case we are going to cursor (or to - bottom) and we will face a macro *) - match self#grafite_status#proof_status with - Incomplete_proof p -> - userGoal <- - (try Some (Continuationals.Stack.find_goal p.stack) - with Failure _ -> None) - | _ -> userGoal <- None - - method private _retract offset grafite_status new_statements - new_history - = - let cur_grafite_status = - match history with s::_ -> s | [] -> assert false - in - LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status; - GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status (); + buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext + + method private _retract offset status new_statements new_history = + NCicLibrary.time_travel status; statements <- new_statements; history <- new_history; self#moveMark (- offset) @@ -822,7 +706,7 @@ object (self) method retract () = try - let cmp,new_statements,new_history,grafite_status = + let cmp,new_statements,new_history,status = match statements,history with stat::statements, _::(status::_ as history) -> assert (Glib.Utf8.validate stat); @@ -830,8 +714,7 @@ object (self) | [],[_] -> raise Margin | _,_ -> assert false in - self#_retract cmp grafite_status new_statements - new_history; + self#_retract cmp status new_statements new_history; self#notify with | Margin -> self#notify @@ -898,7 +781,10 @@ object (self) buffer#move_mark mark mark_position; source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark; end; - while Glib.Main.pending () do ignore(Glib.Main.iteration false); done + let time0 = Unix.gettimeofday () in + GtkThread.sync (fun () -> while Glib.Main.pending () do ignore(Glib.Main.iteration false); done) (); + let time1 = Unix.gettimeofday () in + HLog.debug ("... refresh done in " ^ string_of_float (time1 -. time0) ^ "s") method clean_dirty_lock = let lock_mark_iter = buffer#get_iter_at_mark (`MARK locked_mark) in @@ -911,13 +797,12 @@ object (self) observers <- o :: observers method private notify = - let grafite_status = self#grafite_status in - List.iter (fun o -> o grafite_status) observers + let status = self#status in + List.iter (fun o -> o status) observers - method loadFromString s = - buffer#set_text s; - self#reset_buffer; - buffer#set_modified true + method activate = + NCicLibrary.replace self#status; + self#notify method loadFromFile f = buffer#set_text (HExtlib.input_file f); @@ -925,17 +810,23 @@ object (self) buffer#set_modified false method assignFileName file = - let file = - match file with - | Some f -> Some (Librarian.absolutize f) - | None -> None - in - filename_ <- file; - include_paths_ <- - (match file with Some file -> read_include_paths file | None -> []); - self#reset_buffer; - Sys.chdir self#curdir; - HLog.debug ("Moving to " ^ Sys.getcwd ()) + match file with + None -> + tab_label#set_text default_fname; + filename_ <- None; + include_paths_ <- []; + self#reset_buffer + | Some file -> + let f = Librarian.absolutize file in + tab_label#set_text (Filename.basename f); + filename_ <- Some f; + include_paths_ <- MatitaEngine.read_include_paths ~include_paths:[] f; + self#reset_buffer + + method set_star b = + tab_label#set_text ((if b then "*" else "")^Filename.basename self#filename); + tab_label#misc#set_tooltip_text + ("URI: " ^ self#buri_of_current_file ^ "\nPATH: " ^ self#filename); method saveToFile () = if self#has_name then @@ -943,7 +834,7 @@ object (self) output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); close_out oc; - set_star false; + self#set_star false; buffer#set_modified false else HLog.error "Can't save, no filename selected" @@ -951,18 +842,17 @@ object (self) method private _saveToBackupFile () = if buffer#modified then begin - let f = self#filename in + let f = self#filename ^ "~" in let oc = open_out f in output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); close_out oc; - HLog.debug ("backup " ^ f ^ " saved") + HLog.debug ("backup " ^ f ^ " saved") end method private reset_buffer = statements <- []; - history <- [ initial_statuses (Some self#grafite_status) self#buri_of_current_file ]; - userGoal <- None; + history <- [ initial_statuses (Some self#status) self#buri_of_current_file ]; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter @@ -978,7 +868,7 @@ object (self) let template = HExtlib.input_file BuildTimeConf.script_template in buffer#insert ~iter:(buffer#get_iter `START) template; buffer#set_modified false; - set_star false + self#set_star false; method goto (pos: [`Top | `Bottom | `Cursor]) () = try @@ -1037,9 +927,9 @@ object (self) in let rec back_until_cursor len = (* go backward until locked < cursor *) function - statements, ((grafite_status)::_ as history) + statements, ((status)::_ as history) when len <= 0 -> - self#_retract (icmp - len) grafite_status statements + self#_retract (icmp - len) status statements history | statement::tl1, _::tl2 -> back_until_cursor (len - MatitaGtkMisc.utf8_string_length statement) (tl1,tl2) @@ -1063,56 +953,30 @@ object (self) 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 - | Incomplete_proof _ -> true - | Intermediate _ -> assert false - -(* method proofStatus = MatitaTypes.get_proof_status self#status *) - method proofMetasenv = GrafiteTypes.get_proof_metasenv self#grafite_status - - method proofContext = - match userGoal with - None -> [] - | Some n -> GrafiteTypes.get_proof_context self#grafite_status n - - method proofConclusion = - match userGoal with - None -> assert false - | Some n -> - GrafiteTypes.get_proof_conclusion self#grafite_status n - - method stack = GrafiteTypes.get_stack self#grafite_status - method setGoal n = userGoal <- n - method goal = userGoal - method bos = match history with | _::[] -> true | _ -> false method eos = - let rec is_there_only_comments lexicon_status s = + let rec is_there_only_comments status s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; - let lexicon_status,st = - GrafiteParser.parse_statement (Ulexing.from_utf8_string s) - ~include_paths:self#include_paths lexicon_status - in - match st with - | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> + let strm = + GrafiteParser.parsable_statement status + (Ulexing.from_utf8_string s)in + match GrafiteParser.parse_statement status strm with + | GrafiteAst.Comment (loc,_) -> let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in (* CSC: why +1 in the following lines ???? *) let parsed_text_length = parsed_text_length + 1 in let remain_len = String.length s - parsed_text_length in let next = String.sub s parsed_text_length remain_len in - is_there_only_comments lexicon_status next - | GrafiteParser.LNone _ - | GrafiteParser.LSome (GrafiteAst.Executable _) -> false + is_there_only_comments status next + | GrafiteAst.Executable _ -> false in - try is_there_only_comments self#grafite_status self#getFuture + try is_there_only_comments self#status self#getFuture with - | LexiconEngine.IncludedFileNotCompiled _ + | NCicLibrary.IncludedFileNotCompiled _ | HExtlib.Localized _ | CicNotationParser.Parse_error _ -> false | Margin | End_of_file -> true @@ -1125,17 +989,37 @@ object (self) HLog.debug (sprintf "%d statements:" (List.length statements)); List.iter HLog.debug statements; HLog.debug ("Current file name: " ^ self#filename); + + method has_parent (p : GObj.widget) = parent#coerce#misc#get_oid = p#misc#get_oid end -let _script = ref None +let _script = ref [] -let script ~source_view ~mathviewer ~urichooser ~ask_confirmation ~set_star () +let script ~parent ~tab_label () = - let s = new script - ~source_view ~mathviewer ~ask_confirmation ~urichooser ~set_star () - in - _script := Some s; + let s = new script ~parent ~tab_label () in + _script := s::!_script; s -let current () = match !_script with None -> assert false | Some s -> s +let at_page page = + let notebook = (MatitaMisc.get_gui ())#main#scriptNotebook in + let parent = notebook#get_nth_page page in + try + List.find (fun s -> s#has_parent parent) !_script + with + Not_found -> assert false +;; + +let current () = + at_page ((MatitaMisc.get_gui ())#main#scriptNotebook#current_page) + +let destroy page = + let s = at_page page in + _script := List.filter ((<>) s) !_script +;; + +let iter_scripts f = List.iter f !_script;; +let _ = + CicMathView.register_matita_script_current (current :> unit -> < advance: ?statement:string -> unit -> unit; status: GrafiteTypes.status >) +;;