From 0aa993bb1d23567612aa5d63fab74ef6fb918c0d Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 9 Nov 2011 14:19:12 +0000 Subject: [PATCH] Matitaweb: 1) Adds a feature to enrich automation statements with their trace (after successful execution) 2) Introduces a different syntax (/... trace lemma1, lemma2 .../) for system-generated traces (as opposed to user-provided) 3) Graphical update hiding system-generated traces (they are provided as a tooltip for inspection, when hovering with the mouse pointer on the tactic) 4) Fixes a bug in the computation of the cursor position in the script. --- matitaB/components/grafite/grafiteAst.ml | 2 +- .../grafite_engine/grafiteEngine.ml | 2 +- .../grafite_parser/grafiteParser.ml | 21 ++-- .../ng_disambiguation/nCicDisambiguate.ml | 4 +- matitaB/components/ng_tactics/nnAuto.ml | 32 ++++-- matitaB/matita/index.html | 4 +- matitaB/matita/jquery.tooltip.css | 9 ++ matitaB/matita/jquery.tooltip.min.js | 19 ++++ matitaB/matita/layout.js | 19 ++-- matitaB/matita/matitadaemon.ml | 107 +++++++++++++----- matitaB/matita/matitaweb.css | 19 +++- matitaB/matita/matitaweb.js | 45 ++++++-- 12 files changed, 210 insertions(+), 73 deletions(-) create mode 100644 matitaB/matita/jquery.tooltip.css create mode 100644 matitaB/matita/jquery.tooltip.min.js diff --git a/matitaB/components/grafite/grafiteAst.ml b/matitaB/components/grafite/grafiteAst.ml index bb496f2c0..bc001d173 100644 --- a/matitaB/components/grafite/grafiteAst.ml +++ b/matitaB/components/grafite/grafiteAst.ml @@ -32,7 +32,7 @@ type loc = Stdpp.location type npattern = NotationPt.term option * (string * NotationPt.term) list * NotationPt.term option -type auto_params = NotationPt.term list option * (string*string) list +type auto_params = (bool * NotationPt.term list) option * (string*string) list type ntactic = | NApply of loc * NotationPt.term diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml index 1aa234211..5ac28559d 100644 --- a/matitaB/components/grafite_engine/grafiteEngine.ml +++ b/matitaB/components/grafite_engine/grafiteEngine.ml @@ -354,7 +354,7 @@ let eval_ng_tac tac = ) seqs) | GrafiteAst.NAuto (_loc, (None,a)) -> NnAuto.auto_tac ~params:(None,a) ?trace_ref:None - | GrafiteAst.NAuto (_loc, (Some l,a)) -> + | GrafiteAst.NAuto (_loc, (Some (_,l),a)) -> NnAuto.auto_tac ~params:(Some List.map (fun x -> "",0,x) l,a) ?trace_ref:None | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false diff --git a/matitaB/components/grafite_parser/grafiteParser.ml b/matitaB/components/grafite_parser/grafiteParser.ml index 1010e2c83..b72fecb76 100644 --- a/matitaB/components/grafite_parser/grafiteParser.ml +++ b/matitaB/components/grafite_parser/grafiteParser.ml @@ -211,13 +211,13 @@ EXTEND | None -> G.NTactic(loc, [G.NAuto(loc,(None,["depth",depth]@params))]) - | Some (`Univ univ) -> + | Some (b,`Univ univ) -> G.NTactic(loc, - [G.NAuto(loc,(Some univ,["depth",depth]@params))]) - | Some `EmptyUniv -> + [G.NAuto(loc,(Some (b,univ),["depth",depth]@params))]) + | Some (b,`EmptyUniv) -> G.NTactic(loc, - [G.NAuto(loc,(Some [],["depth",depth]@params))]) - | Some `Trace -> + [G.NAuto(loc,(Some (b,[]),["depth",depth]@params))]) + | Some (b,`Trace) -> G.NMacro(loc, G.NAutoInteractive (loc, (None,["depth",depth]@params)))) | IDENT "intros" -> G.NMacro (loc, G.NIntroGuess loc) @@ -293,10 +293,13 @@ EXTEND i = auto_fixed_param -> i,"" | i = auto_fixed_param ; SYMBOL "="; v = [ v = int -> string_of_int v | v = IDENT -> v ] -> i,v ]; - just = OPT [ IDENT "by"; by = - [ univ = tactic_term_list1 -> `Univ univ - | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv - | SYMBOL "_" -> `Trace ] -> by ] -> just,params + just = OPT [ is_user_trace = + [ IDENT "by" -> true + | IDENT "trace" -> false ]; + by = + [ univ = tactic_term_list1 -> `Univ univ + | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv + | SYMBOL "_" -> `Trace ] -> is_user_trace,by ] -> just,params ] ]; diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml index 95ee85c24..1d3242804 100644 --- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml @@ -18,8 +18,8 @@ open DisambiguateTypes module Ast = NotationPt module NRef = NReference -let debug_print s = prerr_endline (Lazy.force s);; -(* let debug_print _ = ();; *) +(*let debug_print s = prerr_endline (Lazy.force s);;*) +let debug_print _ = ();; let cic_name_of_name = function | Ast.Ident (n,_) -> n diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index a85c18205..38e19486b 100644 --- a/matitaB/components/ng_tactics/nnAuto.ml +++ b/matitaB/components/ng_tactics/nnAuto.ml @@ -14,7 +14,7 @@ open Printf let print ?(depth=0) s = prerr_endline (String.make (2*depth) ' '^Lazy.force s) let noprint ?(depth=0) _ = () -let debug_print = noprint +let debug_print = print open Continuationals.Stack open NTacStatus @@ -146,9 +146,11 @@ let is_a_fact_ast status subst metasenv ctx cand = let ty = NCicTypeChecker.typeof status subst metasenv ctx t in is_a_fact status (mk_cic_term ctx ty) -let current_goal status = +let current_goal ?(single_goal=true) status = let open_goals = head_goals status#stack in - assert (List.length open_goals = 1); + if single_goal + then assert (List.length open_goals = 1) + else assert (List.length open_goals >= 1); let open_goal = List.hd open_goals in let gty = get_goalty status open_goal in let ctx = ctx_of gty in @@ -854,7 +856,7 @@ type cache = let add_to_trace status ~depth cache t = match t with | Ast.NRef _ -> - debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t)); + print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t)); {cache with trace = t::cache.trace} | Ast.NCic _ (* local candidate *) | _ -> (*not an application *) cache @@ -1732,15 +1734,22 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = (NDiscriminationTree.TermSet.elements t)) ))); *) - let candidates = + (* To allow using Rels in the user-specified candidates, we need a context + * but in the case where multiple goals are open, there is no single context + * to type the Rels. At this time, we require that Rels be typed in the + * context of the first selected goal *) + let _,ctx,_ = current_goal ~single_goal:false status in + let status, candidates = match univ with - | None -> None + | None -> status, None | Some l -> - let to_Ast t = - let status, res = disambiguate status [] t None in - let _,res = term_of_cic_term status res (ctx_of res) - in Ast.NCic res - in Some (List.map to_Ast l) + let to_Ast (st,l) t = + let st, res = disambiguate st ctx t None in + let st, res = term_of_cic_term st res (ctx_of res) + in (st, Ast.NCic res::l) + in + let status, l' = List.fold_left to_Ast (status,[]) l in + status, Some l' in let depth = int "depth" flags 3 in let size = int "size" flags 10 in @@ -1779,6 +1788,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = | Proved (s,trace) -> debug_print (lazy ("proved at depth " ^ string_of_int x)); List.iter (toref incr_uses statistics) trace; + let _ = debug_print (pptrace status trace) in let trace = cleanup_trace s trace in let _ = debug_print (pptrace status trace) in let stack = diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html index 067189d73..21ffb0e5c 100644 --- a/matitaB/matita/index.html +++ b/matitaB/matita/index.html @@ -2,17 +2,19 @@ + + - + diff --git a/matitaB/matita/jquery.tooltip.css b/matitaB/matita/jquery.tooltip.css new file mode 100644 index 000000000..feeca8370 --- /dev/null +++ b/matitaB/matita/jquery.tooltip.css @@ -0,0 +1,9 @@ +#tooltip { + position: absolute; + z-index: 3000; + border: 1px solid #111; + background-color: #ffffbf; + padding: 5px; + /* opacity: 0.85; */ +} +#tooltip h3, #tooltip div { margin: 0; } diff --git a/matitaB/matita/jquery.tooltip.min.js b/matitaB/matita/jquery.tooltip.min.js new file mode 100644 index 000000000..a8d0cc69a --- /dev/null +++ b/matitaB/matita/jquery.tooltip.min.js @@ -0,0 +1,19 @@ +/* + * jQuery Tooltip plugin 1.3 + * + * http://bassistance.de/jquery-plugins/jquery-plugin-tooltip/ + * http://docs.jquery.com/Plugins/Tooltip + * + * Copyright (c) 2006 - 2008 Jörn Zaefferer + * + * $Id: jquery.tooltip.js 5741 2008-06-21 15:22:16Z joern.zaefferer $ + * + * Dual licensed under the MIT and GPL licenses: + * http://www.opensource.org/licenses/mit-license.php + * http://www.gnu.org/licenses/gpl.html + */;(function($){var helper={},current,title,tID,IE=$.browser.msie&&/MSIE\s(5\.5|6\.)/.test(navigator.userAgent),track=false;$.tooltip={blocked:false,defaults:{delay:200,fade:false,showURL:true,extraClass:"",top:15,left:15,id:"tooltip"},block:function(){$.tooltip.blocked=!$.tooltip.blocked;}};$.fn.extend({tooltip:function(settings){settings=$.extend({},$.tooltip.defaults,settings);createHelper(settings);return this.each(function(){$.data(this,"tooltip",settings);this.tOpacity=helper.parent.css("opacity");this.tooltipText=this.title;$(this).removeAttr("title");this.alt="";}).mouseover(save).mouseout(hide).click(hide);},fixPNG:IE?function(){return this.each(function(){var image=$(this).css('backgroundImage');if(image.match(/^url\(["']?(.*\.png)["']?\)$/i)){image=RegExp.$1;$(this).css({'backgroundImage':'none','filter':"progid:DXImageTransform.Microsoft.AlphaImageLoader(enabled=true, sizingMethod=crop, src='"+image+"')"}).each(function(){var position=$(this).css('position');if(position!='absolute'&&position!='relative')$(this).css('position','relative');});}});}:function(){return this;},unfixPNG:IE?function(){return this.each(function(){$(this).css({'filter':'',backgroundImage:''});});}:function(){return this;},hideWhenEmpty:function(){return this.each(function(){$(this)[$(this).html()?"show":"hide"]();});},url:function(){return this.attr('href')||this.attr('src');}});function createHelper(settings){if(helper.parent)return;helper.parent=$('

').appendTo(document.body).hide();if($.fn.bgiframe)helper.parent.bgiframe();helper.title=$('h3',helper.parent);helper.body=$('div.body',helper.parent);helper.url=$('div.url',helper.parent);}function settings(element){return $.data(element,"tooltip");}function handle(event){if(settings(this).delay)tID=setTimeout(show,settings(this).delay);else +show();track=!!settings(this).track;$(document.body).bind('mousemove',update);update(event);}function save(){if($.tooltip.blocked||this==current||(!this.tooltipText&&!settings(this).bodyHandler))return;current=this;title=this.tooltipText;if(settings(this).bodyHandler){helper.title.hide();var bodyContent=settings(this).bodyHandler.call(this);if(bodyContent.nodeType||bodyContent.jquery){helper.body.empty().append(bodyContent)}else{helper.body.html(bodyContent);}helper.body.show();}else if(settings(this).showBody){var parts=title.split(settings(this).showBody);helper.title.html(parts.shift()).show();helper.body.empty();for(var i=0,part;(part=parts[i]);i++){if(i>0)helper.body.append("
");helper.body.append(part);}helper.body.hideWhenEmpty();}else{helper.title.html(title).show();helper.body.hide();}if(settings(this).showURL&&$(this).url())helper.url.html($(this).url().replace('http://','')).show();else +helper.url.hide();helper.parent.addClass(settings(this).extraClass);if(settings(this).fixPNG)helper.parent.fixPNG();handle.apply(this,arguments);}function show(){tID=null;if((!IE||!$.fn.bgiframe)&&settings(current).fade){if(helper.parent.is(":animated"))helper.parent.stop().show().fadeTo(settings(current).fade,current.tOpacity);else +helper.parent.is(':visible')?helper.parent.fadeTo(settings(current).fade,current.tOpacity):helper.parent.fadeIn(settings(current).fade);}else{helper.parent.show();}update();}function update(event){if($.tooltip.blocked)return;if(event&&event.target.tagName=="OPTION"){return;}if(!track&&helper.parent.is(":visible")){$(document.body).unbind('mousemove',update)}if(current==null){$(document.body).unbind('mousemove',update);return;}helper.parent.removeClass("viewport-right").removeClass("viewport-bottom");var left=helper.parent[0].offsetLeft;var top=helper.parent[0].offsetTop;if(event){left=event.pageX+settings(current).left;top=event.pageY+settings(current).top;var right='auto';if(settings(current).positionLeft){right=$(window).width()-left;left='auto';}helper.parent.css({left:left,right:right,top:top});}var v=viewport(),h=helper.parent[0];if(v.x+v.cx" in + let res = Str.global_replace patt4 ">" s in + let res = Str.global_replace patt3 "<" res in + let res = Str.global_replace patt2 ">" res in + let res = Str.global_replace patt1 "<" res in + res +;; + (* adds a user to the commit queue; concurrent instances possible, so we * enclose the update in a CS *) @@ -143,31 +155,88 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script match statement with | `Raw text -> (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *) + prerr_endline ("raw text = " ^ text); let strm = GrafiteParser.parsable_statement status (Ulexing.from_utf8_string text) in + prerr_endline "before get_ast"; let ast = MatitaEngine.get_ast status include_paths strm in + prerr_endline "after get_ast"; ast, text | `Ast (st, text) -> st, text in + + (* do we want to generate a trace? *) + let is_auto (l,a) = + not (List.mem_assoc "demod" a || List.mem_assoc "paramod" a || + List.mem_assoc "fast_paramod" a || List.assoc "depth" a = "1" || + l <> None) + in + + let get_param a param = + try + Some (param ^ "=" ^ List.assoc param a) + with Not_found -> None + in + let floc = match ast with | GrafiteAst.Executable (loc, _) | GrafiteAst.Comment (loc, _) -> loc in - let _,lend = HExtlib.loc_of_floc floc in + let lstart,lend = HExtlib.loc_of_floc floc in let parsed_text, _parsed_text_len = HExtlib.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in + let parsed_text_len = utf8_length parsed_text in let byte_parsed_text_len = String.length parsed_text in let unparsed_txt' = String.sub unparsed_text byte_parsed_text_len (String.length unparsed_text - byte_parsed_text_len) in + let pre = Netconversion.ustring_sub `Enc_utf8 0 lstart parsed_text in + + let mk_univ trace = + let href r = + Printf.sprintf "\005A href=\"%s\"\006%s\005/A\006" + (NReference.string_of_reference r) (NCicPp.r2s status true r) + in + if trace = [] then "{}" + else String.concat ", " + (HExtlib.filter_map (function + | NotationPt.NRef r -> Some (href r) + | _ -> None) + trace) + in - let status = - MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast) - in - (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*) - utf8_length parsed_text + match ast with + | GrafiteAst.Executable (_, + GrafiteAst.NTactic (_, + [GrafiteAst.NAuto (_, (l,a as auto_params))])) when is_auto auto_params + -> + let l = match l with + | None -> None + | Some _,l' -> Some (List.map (fun x -> "",0,x) l') + in + let trace_ref = ref [] in + let status = NnAuto.auto_tac ~params:(l,a) ~trace_ref status in + let new_parsed_text = pre ^ (Printf.sprintf + "/\005span class='autotactic'\006%s\005span class='autotrace'\006 trace %s\005/span\006\005/span\006/" + (String.concat " " + (List.assoc "depth" a:: + HExtlib.filter_map (get_param a) ["width";"size"])) + (mk_univ !trace_ref)) + in + (status,new_parsed_text, unparsed_txt'),parsed_text_len + | _ -> + let status = + MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast) + in + let new_parsed_text = Ulexing.from_utf8_string parsed_text in + let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in + let outstr = ref "" in + ignore (SmallLexer.mk_small_printer interpr outstr new_parsed_text); + prerr_endline ("baseuri after advance = " ^ status#baseuri); + (* prerr_endline ("parser output: " ^ !outstr); *) + (status,!outstr, unparsed_txt'),parsed_text_len (*let save_moo status = let script = MatitaScript.current () in @@ -239,18 +308,6 @@ let output_status s = (* prerr_endline ("sending metasenv:\n" ^ res); res *) ;; -let html_of_matita s = - let patt1 = Str.regexp "\005" in - let patt2 = Str.regexp "\006" in - let patt3 = Str.regexp "<" in - let patt4 = Str.regexp ">" in - let res = Str.global_replace patt4 ">" s in - let res = Str.global_replace patt3 "<" res in - let res = Str.global_replace patt2 ">" res in - let res = Str.global_replace patt1 "<" res in - res -;; - let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";; let first_line s = @@ -346,7 +403,7 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let advance0 sid text = let status = MatitaAuthentication.get_status sid in let status = status#reset_disambiguate_db () in - let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len = + let (st,new_statements,new_unparsed),parsed_len = try eval_statement !include_paths (*buffer*) status (`Raw text) with @@ -414,16 +471,10 @@ let advance0 sid text = in raise (Ambiguous strchoices) (* | End_of_file -> ... *) in - let stringbuf = Ulexing.from_utf8_string new_statements in - let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in - let outstr = ref "" in - ignore (SmallLexer.mk_small_printer interpr outstr stringbuf); - prerr_endline ("baseuri after advance = " ^ st#baseuri); - (* prerr_endline ("parser output: " ^ !outstr); *) MatitaAuthentication.set_status sid st; parsed_len, Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false - () (html_of_matita !outstr), new_unparsed, st + () (html_of_matita new_statements), new_unparsed, st let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in @@ -721,14 +772,14 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed with - | End_of_file -> + | (* End_of_file *) _ -> let status = MatitaAuthentication.get_status sid in GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string status#baseuri) status; if parsed_len > 0 then MatitaAuthentication.set_history sid (status::history); parsed_len, parsed_txt - | _ -> parsed_len, parsed_txt + (*| _ -> parsed_len, parsed_txt*) in (* cgi # set_header diff --git a/matitaB/matita/matitaweb.css b/matitaB/matita/matitaweb.css index 4b4f2a7d9..cc9629e87 100644 --- a/matitaB/matita/matitaweb.css +++ b/matitaB/matita/matitaweb.css @@ -191,7 +191,7 @@ div.toolbar { margin-left: auto; margin-right: auto; height:100%; - width:300px; + width:350px; float:left; } @@ -219,8 +219,8 @@ div.scriptarea { margin-right: auto;*/ height:100%; width:67%; - min-width:67%; - max-width:67%; +/* min-width:67%; + max-width:67%; */ float:left; } @@ -233,8 +233,8 @@ div.sidearea { margin-right: auto;*/ height:100%; width:33%; - min-width:33%; - max-width:33%; +/* min-width:33%; + max-width:33%; */ float:right; } @@ -246,6 +246,15 @@ div.context { overflow: auto; } +span.autotactic { + color: green; + font-weight: bold; +} + +span.autotrace { + display:none; +} + span.activegoal { color: red; font-weight: bold; diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index c98937735..cd1e624e1 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -85,9 +85,33 @@ function initialize() // initialize keyboard events in the unlocked script init_keyboard(unlocked); + + init_autotraces(); + } } +function init_autotraces() { + $("#unlocked .autotactic").tooltip({ + delay: 0, + showURL: false, + bodyHandler: function() { + return (trace_of($(this)[0])); + } + }); + $("#locked .autotactic").tooltip({ + delay: 0, + showURL: false, + bodyHandler: function() { + return (trace_of($(this)[0])); + } + }); +} + +function trace_of(node) { + return text_of_html(filterByClass(node.childNodes,"autotrace")[0]); +} + function changeFile(name) { current_fname = name; matitaTitle.innerHTML = "Matita - cic:/matita/" + name; @@ -196,7 +220,7 @@ function strip_tags(tagname,classname) tags[i].parentNode.insertBefore(children[j],tags[i]); } } - for (;tags.length > 0;) { + while (tags.length > 0) { tags[0].parentNode.removeChild(tags[0]); } } @@ -214,9 +238,9 @@ function keypress(e) strip_tags("span","error"); if (s == " ") { j = getCursorPos(); - i = unlocked.innerHTML.lastIndexOf('\\',j); + i = unlocked.innerHTML.html_to_matita().lastIndexOf('\\',j); if (i >= 0) { - match = unlocked.innerHTML.substring(i,j); + match = unlocked.innerHTML.html_to_matita().substring(i,j); sym = unescape_html(lookup_tex(match)); if (sym != "undefined") { if (window.getSelection) { // non IE @@ -575,6 +599,7 @@ function advanceForm1() var len2 = parsedtxt.length; var metasenv = xml.getElementsByTagName("meta"); populate_goalarray(metasenv); + init_autotraces(); statements = listcons(len2,statements); unlocked.scrollIntoView(true); } @@ -674,6 +699,7 @@ function gotoBottom() // len1 = unlocked.innerHTML.length; len2 = parsedtxt.length; metasenv = xml.getElementsByTagName("meta"); + init_autotraces(); populate_goalarray(metasenv); if (len2 > 0) statements = listcons(len2,statements); @@ -708,6 +734,7 @@ function gotoTop() unlocked.innerHTML = lockedbackup + unlocked.innerHTML; lockedbackup = ""; locked.innerHTML = lockedbackup; + init_autotraces(); hideSequent(); unlocked.scrollIntoView(true); } else { @@ -744,12 +771,14 @@ function gotoPos(offset) unlocked.scrollIntoView(true); // la populate non andrebbe fatta a ogni passo if (offset <= len) { + init_autotraces(); populate_goalarray(metasenv); resume(); } else { gotoPos(offset - len); } } else { + init_autotraces(); unlocked.scrollIntoView(true); populate_goalarray(metasenv); resume(); @@ -778,6 +807,7 @@ function retract() locked.innerHTML = lockedbackup; unlocked.innerHTML = statement + unlocked.innerHTML; metasenv = xml.getElementsByTagName("meta"); + init_autotraces(); populate_goalarray(metasenv); unlocked.scrollIntoView(true); } else { @@ -823,6 +853,7 @@ function retrieveFile(thefile) } else { unlocked.innerHTML = xml.childNodes[0].textContent; } + init_autotraces(); } else { debug("file open failed"); @@ -1049,8 +1080,8 @@ function showDialog(title,content,callback) { $('#mask').css({'width':maskWidth,'height':maskHeight}); //transition effect - $('#mask').fadeIn(1000); - $('#mask').fadeTo("slow",0.8); + $('#mask').fadeIn(100); + $('#mask').fadeTo(200,0.8); //Get the window height and width var winH = $(window).height(); @@ -1061,7 +1092,7 @@ function showDialog(title,content,callback) { $('#dialogBox').css('left', winW/2-$('#dialogBox').width()/2); //transition effect - $('#dialogBox').fadeIn(2000); + $('#dialogBox').fadeIn(200); dialogBox.style.display = "block"; } @@ -1117,7 +1148,7 @@ function findNode(list, node, acc) { dup = list[i].cloneNode(true); sandbox.appendChild(dup); // debug("fail " + i + ": " + sandbox.innerHTML); - acc += sandbox.innerHTML.length; + acc += sandbox.innerHTML.html_to_matita().length; sandbox.removeChild(dup); } throw "not found"; -- 2.39.2