From 070bda8035e9ae0d3bfe69110d184bb82183cf46 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 2 Nov 2011 12:52:37 +0000 Subject: [PATCH] Matitaweb: 1) Added button to strip interpretations from the source 2) Fixed some UI bugs --- matitaB/components/extlib/hExtlib.ml | 1 + matitaB/components/extlib/hExtlib.mli | 4 +- .../ng_disambiguation/grafiteDisambiguate.ml | 2 +- matitaB/matita/index.html | 8 ++ matitaB/matita/matitaweb.css | 24 +++++- matitaB/matita/matitaweb.js | 76 ++++++++++++++----- 6 files changed, 91 insertions(+), 24 deletions(-) diff --git a/matitaB/components/extlib/hExtlib.ml b/matitaB/components/extlib/hExtlib.ml index 6b2b68d68..78ac69126 100644 --- a/matitaB/components/extlib/hExtlib.ml +++ b/matitaB/components/extlib/hExtlib.ml @@ -224,6 +224,7 @@ let sharing_map_acc f acc l = !final_acc, if !unchanged then l else l1 ;; +(* expects the list to be sorted *) let rec list_uniq ?(eq=(=)) = function | [] -> [] | h::[] -> [h] diff --git a/matitaB/components/extlib/hExtlib.mli b/matitaB/components/extlib/hExtlib.mli index 394f259e4..27e8a694a 100644 --- a/matitaB/components/extlib/hExtlib.mli +++ b/matitaB/components/extlib/hExtlib.mli @@ -81,8 +81,8 @@ val trim_blanks: string -> string (** strip heading and trailing blanks *) (** {2 List processing} *) -val list_uniq: - ?eq:('a->'a->bool) -> 'a list -> 'a list (** uniq unix filter on lists *) +val list_uniq: + ?eq:('a->'a->bool) -> 'a list -> 'a list (** uniq unix filter on (sorted) lists *) val filter_map: ('a -> 'b option) -> 'a list -> 'b list (** filter + map *) val filter_map_acc: ('acc -> 'a -> ('acc * 'b) option) -> 'acc -> 'a list -> 'acc * 'b list (** fold/filter + map *) diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index b1dc98a1e..544128bef 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -297,7 +297,7 @@ let diff_obj loc o1 o2 = match o1,o2 with let rec find_diffs l = let loc,_ = List.hd (List.hd l) in let hds = List.map (fun x -> snd (List.hd x)) l in - let uniq_hds = HExtlib.list_uniq hds in + let uniq_hds = HExtlib.list_uniq (List.sort Pervasives.compare hds) in if List.length uniq_hds > 1 then loc, uniq_hds diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html index 80f49ece4..067189d73 100644 --- a/matitaB/matita/index.html +++ b/matitaB/matita/index.html @@ -1,6 +1,7 @@ + @@ -55,6 +56,7 @@ + @@ -110,5 +112,11 @@ + +
+ + +
+ diff --git a/matitaB/matita/matitaweb.css b/matitaB/matita/matitaweb.css index fbc7d22ed..4b4f2a7d9 100644 --- a/matitaB/matita/matitaweb.css +++ b/matitaB/matita/matitaweb.css @@ -59,15 +59,12 @@ div.mainRight { div.dialog { position:absolute; - top: 50%; - left: 50%; width:450px; height:500px; - margin-top: -250px; /*set to a negative number 1/2 of your height*/ - margin-left: -225px; /*set to a negative number 1/2 of your width*/ border: 1px solid #ccc; padding: 3px; background-color: #f3f3f3; + z-index: 9999; } div.diaTitle { @@ -94,6 +91,25 @@ div.diaClose { line-height: 32px } +#mask { + position:absolute; + left:0; + top:0; + z-index:9000; + background-color:#000; + display:none; +} + +#whitemask { + position:absolute; + left:0; + top:0; + z-index:9000; + background-color:#ffffff; + display:none; +} + + a#hlogout { color: inherit; font-weight: bold; diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 44fd608a1..c98937735 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -34,10 +34,10 @@ function unescape_html(s) return text_of_html(u) } -function filterByClass (elements,class){ +function filterByClass (elements,cname){ var itemsfound = new Array; for(var i=0;i 0;) { + tags[0].parentNode.removeChild(tags[0]); + } +} + +function strip_interpr() { + strip_tags("A"); + alert("strip_interpr ended"); } function keypress(e) @@ -201,7 +211,7 @@ function keypress(e) if (!e) e= event; pressmesg('keypress',e); var s = string_of_key(e.charCode); - strip_errors(); + strip_tags("span","error"); if (s == " ") { j = getCursorPos(); i = unlocked.innerHTML.lastIndexOf('\\',j); @@ -623,6 +633,8 @@ function advanceForm1() disambcell.appendChild(okbutton); disambcell.appendChild(cancelbutton); + disable_toparea(); + matita.disambMode = true; updateSide(); } @@ -816,7 +828,7 @@ function retrieveFile(thefile) debug("file open failed"); } }; - dialogBox.style.display = "none"; + abortDialog(); callServer("open",processor,"file=" + escape(thefile)); } @@ -901,7 +913,7 @@ function openDialog() function saveDialog() { callback = function (fname) { - dialogBox.style.display = "none"; + abortDialog(); saveFile(fname, (locked.innerHTML.html_to_matita()).sescape(), (unlocked.innerHTML.html_to_matita()).sescape(), @@ -913,7 +925,7 @@ function saveDialog() function newDialog() { callback = function (fname) { - dialogBox.style.display = "none"; + abortDialog(); saveFile(fname,"","",false,newDialog,true); }; showLibrary("Create new file", callback, newDialog); @@ -1028,15 +1040,34 @@ function showDialog(title,content,callback) { dialogTitle.innerHTML = title; dialogContent.innerHTML = content; dialogBox.callback = callback; - dialogBox.style.display = "block"; -} -function showDisamb(content) { - disambContent.innerHTML = content; - disambBox.style.display = "block"; + //Get the screen height and width + var maskHeight = $(document).height(); + var maskWidth = $(window).width(); + + //Set heigth and width to mask to fill up the whole screen + $('#mask').css({'width':maskWidth,'height':maskHeight}); + + //transition effect + $('#mask').fadeIn(1000); + $('#mask').fadeTo("slow",0.8); + + //Get the window height and width + var winH = $(window).height(); + var winW = $(window).width(); + + //Set the popup window to center + $('#dialogBox').css('top', winH/2-$('#dialogBox').height()/2); + $('#dialogBox').css('left', winW/2-$('#dialogBox').width()/2); + + //transition effect + $('#dialogBox').fadeIn(2000); + + dialogBox.style.display = "block"; } function abortDialog(dialog) { + $('#mask').hide(); dialogBox.style.display = "none"; } @@ -1108,6 +1139,7 @@ function get_checked_index(name) { function cancel_disambiguate() { matita.disambMode = false; + $('#whitemask').hide(); updateSide(); } @@ -1134,6 +1166,7 @@ function do_disambiguate() { unlocked.innerHTML = pre + mid + post; matita.disambMode = false; + $('#whitemask').hide(); updateSide(); } } @@ -1160,3 +1193,12 @@ function delete_session() { delete_cookie("session"); } + +function disable_toparea() { + var offset = $('#toparea').offset(); + $('#whitemask').css('top',offset.top); + $('#whitemask').css('left',offset.left); + $('#whitemask').css('width',$('#toparea').outerWidth() + "px"); + $('#whitemask').css('height',$('#toparea').outerHeight() + "px"); + $('#whitemask').fadeTo('fast',0.7); +} -- 2.39.2