]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: cb4b0c8)
Matitaweb:
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Wed, 2 Nov 2011 12:52:37 +0000 (12:52 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Wed, 2 Nov 2011 12:52:37 +0000 (12:52 +0000)
1) Added button to strip interpretations from the source
2) Fixed some UI bugs

matitaB/components/extlib/hExtlib.ml patch | blob | history
matitaB/components/extlib/hExtlib.mli patch | blob | history
matitaB/components/ng_disambiguation/grafiteDisambiguate.ml patch | blob | history
matitaB/matita/index.html patch | blob | history
matitaB/matita/matitaweb.css patch | blob | history
matitaB/matita/matitaweb.js patch | blob | history

diff --git a/matitaB/components/extlib/hExtlib.ml b/matitaB/components/extlib/hExtlib.ml
index 6b2b68d68c8c75b8b2c1beaf09e43c5afa382c3c..78ac69126e19bc857feb8426b97ce24438142c0b 100644 (file)
--- 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 394f259e4713a648fed880d11a8dcb8f6c432ea8..27e8a694a1b1749dc594d2e697d58d71103adbc9 100644 (file)
--- 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 b1dc98a1e23e46cde8c3e265fed0061327a2af2b..544128befd29ea706c6247c50e2056f38b08ee8b 100644 (file)
--- 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 80f49ece416a748bc209e770b5cd0296259f9141..067189d7382f1418ee04a1031b39b6f11660e1b5 100644 (file)
--- a/matitaB/matita/index.html
+++ b/matitaB/matita/index.html
@@ -1,6 +1,7 @@
 <html>
 
 <head>
+<script type="text/javascript" src="jquery.js"></script>
 <script type="text/javascript" src="utf8MacroTable.js"></script>
 <script type="text/javascript" src="matitaweb.js"></script>
 <script type="text/javascript" src="layout.js"></script>
@@ -55,6 +56,7 @@
            <INPUT type="BUTTON" value="Commit" id="commitbutton" ONCLICK="commitAll()">
            <INPUT type="BUTTON" value="Update" id="updatebutton" ONCLICK="updateAll()">
            <INPUT type="BUTTON" value="Log" id="logbutton" ONCLICK="showLog()">
+           <INPUT type="BUTTON" value="Del hrefs" id="delintbutton" ONCLICK="strip_interpr()">
 <!--      <INPUT type="BUTTON" value="show sequent" id="showseq" ONCLICK="showSequent()">
           <INPUT type="BUTTON" value="hide sequent" id="hideseq" ONCLICK="hideSequent()">
           <INPUT type="BUTTON" value="selection test" id="hideseq" ONCLICK="test()"> -->
@@ -110,5 +112,11 @@
   <INPUT type="button" id="uploadSelect" value="OK" ONCLICK="uploadOK()" style="width:70px">
 </div>
 
+<!-- Mask to cover the whole screen --> 
+  <div id="mask"></div> 
+  
+<!-- Mask to cover the toolbar --> 
+  <div id="whitemask"></div> 
+
  </body>
 </html> 
diff --git a/matitaB/matita/matitaweb.css b/matitaB/matita/matitaweb.css
index fbc7d22ed8e7ffd064a61251dd172a59b7d581ab..4b4f2a7d9606e8634cf677d8b05f456c67b1611f 100644 (file)
--- 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 44fd608a1bbf7b099f495a2789cb6a0242fb1af9..c98937735770f2023f9a2ff585d8510962f8e788 100644 (file)
--- 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<elements.length;i++){
-    if(elements[i].className == class){
+    if(elements[i].className == cname){
       itemsfound.push(elements[i]);
     }
   }
@@ -184,16 +184,26 @@ function lookup_tex(texmacro)
   return unescape(macro2utf8[texmacro]);
 }
 
-function strip_errors() 
+function strip_tags(tagname,classname) 
 {
-    errors = filterByClass(unlocked.getElementsByTagName("span"),"error");
-    for (i = 0; i < errors.length; i++) {
-        children = errors[i].childNodes;
+    var tags = unlocked.getElementsByTagName(tagname);
+    if (is_defined(classname)) {
+       tags = filterByClass(tags,classname);
+    }
+    for (i = 0; i < tags.length; i++) {
+        var children = tags[i].childNodes;
         for (j = 0; j < children.length; j++) {
-            unlocked.insertBefore(children[j],errors[i]);
+            tags[i].parentNode.insertBefore(children[j],tags[i]);
        }
-        unlocked.removeChild(errors[i]);
     }
+    for (;tags.length > 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);
+}
Unnamed repository; edit this file 'description' to name the repository.