1) removed many debug prints

2) solved a bug in automation (we had forgotten to saturate clauses in
forward_infer_step, a mistake that prevented equations from being
indexed, resulting in almost certain failure of automation).
3) disabled alpha_eq in NCicBlob.compare, because it now requires a
status containing the correct environment, which can't be guessed
inside compare (enabling alpha_eq results in the automation
sporadically failing).

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index d724acf85d21d0cf014cf928c97bbc70b379cda6..13c70be473f506f435a311467dbd4e624b35842d 100644 (file)
--- a/matitaB/components/content_pres/termContentPres.ml
+++ b/matitaB/components/content_pres/termContentPres.ml
@@ -474,7 +474,7 @@ let rec pp_ast1 status term =
     | NotationEnv.DisambiguationValue _ as v -> v
   in
   let ast_env_of_env env =
-    prerr_endline ("### pp_env: " ^ NotationPp.pp_env status env);
+    (* prerr_endline ("### pp_env: " ^ NotationPp.pp_env status env); *)
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
   in
 (* prerr_endline ("### pattern matching from 2 to 1 on term " ^

diff --git a/matitaB/components/ng_library/nCicLibrary.ml b/matitaB/components/ng_library/nCicLibrary.ml
index 47a62c048c2bb78ebfd9e5a0cd83f759ebf40069..201b5ac082b8a425726a4859db1c6c2f371f9a62 100644 (file)
--- a/matitaB/components/ng_library/nCicLibrary.ml
+++ b/matitaB/components/ng_library/nCicLibrary.ml
@@ -56,7 +56,7 @@ let ng_path_of_baseuri ?(no_suffix=false) user baseuri =
  let path = String.sub uri 4 (String.length uri - 4) in
  let path = match user with
  | Some u -> "/" ^ u ^ path
- | _ -> path
+ | _ -> prerr_endline "WARNING: ng_path_of_baseuri called without a uid"; path
  in
  let path = Helm_registry.get "matita.basedir" ^ path in
  let dirname = Filename.dirname path in
@@ -361,7 +361,9 @@ let resolve st name =
    (fun (_,name',nref) -> if name'=name then Some nref else None)
    (!(st#lib_db.local_aliases) @ get_global_aliases ())
  with
-  Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name))
+  Not_found -> 
+   (prerr_endline ("can't resolve object " ^ name);
+    raise (NCicEnvironment.ObjectNotFound (lazy name)))
 ;;
 
 let aliases_of st uri =
@@ -428,7 +430,8 @@ let get_obj status u =
  with Not_found ->*)
   try fetch_obj (status#user) status u
   with Sys_error _ ->
-   raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u)))
+   (prerr_endline ("can't fetch object " ^ NUri.string_of_uri u);
+   raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u))))
 ;;
 
 NCicEnvironment.set_get_obj 

diff --git a/matitaB/components/ng_paramodulation/nCicBlob.ml b/matitaB/components/ng_paramodulation/nCicBlob.ml
index beef0ae453ba6ce55a80b1bd411b3603effb7630..14454c58b2b0c571a9fe7d62a0095f32d8a09d7c 100644 (file)
--- a/matitaB/components/ng_paramodulation/nCicBlob.ml
+++ b/matitaB/components/ng_paramodulation/nCicBlob.ml
@@ -11,15 +11,15 @@
 
 (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *)
 
-let eqPref = ref (fun _ -> assert false);;
-let set_eqP t = eqPref := fun _ -> t;;
-
-let default_eqP() =
+let default_eqP =
   let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in
   let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
     NCic.Const ref
 ;;
 
+let eqPref = ref default_eqP;;
+let set_eqP t = eqPref := t;;
+
 let equivalence_relation =
   let uri = NUri.uri_of_string "cic:/matita/ng/properties/relations/eq_rel.con"
   in
@@ -84,20 +84,22 @@ with type t = NCic.term and type input = NCic.term = struct
        
   ;;
   
-  let compare x y = 
+  (* let compare x y = 
     (* CSC: NCicPp.status is the best I can put here *)
     (* WR: and I can't guess a user id, so I must put None *)
     if NCicReduction.alpha_eq (new NCicPp.status None) [] [] [] x y  then 0 
     (* if x = y  then 0 *)
     else compare x y
-  ;;
+  ;; *)
 
-  let eqP = (!eqPref)()
+  let eqP = fun () -> !eqPref
   ;;
 
   let is_eq = function
-    | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt ->
+    | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq (eqP()) eqt ->
         Some (ty,l,r) 
+    | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] ->
+        None
 (*
     | Terms.Node [ Terms.Leaf eqt ; _; Terms.Node [Terms.Leaf eqt2 ; ty]; l; r]
        when eq equivalence_relation eqt && eq setoid_eq eqt2 ->

diff --git a/matitaB/components/ng_paramodulation/nCicParamod.ml b/matitaB/components/ng_paramodulation/nCicParamod.ml
index 0f92c66209f08838469c5ded84e0284ad56b1005..5906bc06d3989b27c629a8ef4bbf8a952ec85313 100644 (file)
--- a/matitaB/components/ng_paramodulation/nCicParamod.ml
+++ b/matitaB/components/ng_paramodulation/nCicParamod.ml
@@ -92,14 +92,17 @@ module P = NCicParamod
 type state = P.state
 let empty_state = P.empty_state
 
+let size_of_state = P.size_of_state
+
 let forward_infer_step status metasenv subst context s t ty =
   let bag = P.bag_of_state s in
   let saturate (t,ty) = 
     NCicBlob.saturate status metasenv subst context t ty in
-  let bag,clause = P.mk_passive bag (t,ty) in
+  let bag,clause = P.mk_passive bag (saturate (t,ty)) in
     if Terms.is_eq_clause clause then
-      P.forward_infer_step (P.replace_bag s bag) clause 0
-    else (debug (lazy "not eq"); s)
+      ((*prerr_endline "is eq";*)
+      P.forward_infer_step (P.replace_bag s bag) clause 0)
+    else ((*print (lazy "not eq");*) s)
 ;;
 
 let index_obj status s uri =
@@ -152,7 +155,7 @@ let is_equation status metasenv subst context ty =
     NCicMetaSubst.saturate status ~delta:0 metasenv subst context
       ty 0 
   in match hty with
-    | NCic.Appl (eq ::tl) when eq = CB.eqP -> true
+    | NCic.Appl (eq ::tl) when eq = CB.eqP() -> true
     | _ -> false
 ;;
 

diff --git a/matitaB/components/ng_paramodulation/nCicParamod.mli b/matitaB/components/ng_paramodulation/nCicParamod.mli
index b46d0ade0d0b650764322e8d73d2023f1e5a65de..93d322dd1007786cfaf394b2fbfd25004eeec145 100644 (file)
--- a/matitaB/components/ng_paramodulation/nCicParamod.mli
+++ b/matitaB/components/ng_paramodulation/nCicParamod.mli
@@ -19,6 +19,7 @@ val nparamod :
 
 type state 
 val empty_state: state
+val size_of_state: state -> int * int
 val forward_infer_step: 
   #NCicCoercion.status ->
   NCic.metasenv -> 

diff --git a/matitaB/components/ng_paramodulation/paramod.ml b/matitaB/components/ng_paramodulation/paramod.ml
index 33f802f7f036caf9152d65de93a4c3cabce55842..83845673b3142cf1805323034983fc316bf957c1 100644 (file)
--- a/matitaB/components/ng_paramodulation/paramod.ml
+++ b/matitaB/components/ng_paramodulation/paramod.ml
@@ -30,6 +30,7 @@ module type Paramod =
     type bag = t Terms.bag * int
     type state
     val empty_state : state
+    val size_of_state : state -> int*int
     val bag_of_state : state -> bag
     val replace_bag: state -> bag -> state
     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
@@ -336,6 +337,8 @@ module Paramod (B : Orderings.Blob) = struct
     add_passive_goals g_passives new_goals
   ;;
 
+  let size_of_state (_,_,(a,_),p,_,_) = List.length a, passive_set_cardinal p;;
+
   let debug_status (_,_,actives,passives,g_actives,g_passives) =
     lazy
       ((Printf.sprintf "Number of active goals : %d\n"

diff --git a/matitaB/components/ng_paramodulation/paramod.mli b/matitaB/components/ng_paramodulation/paramod.mli
index 60691a57c0bd843bdbde2c114d5b8cb9147fb5a9..d91ba1b349b939b06a3bc5154458acbc981ce6a4 100644 (file)
--- a/matitaB/components/ng_paramodulation/paramod.mli
+++ b/matitaB/components/ng_paramodulation/paramod.mli
@@ -24,6 +24,7 @@ module type Paramod =
       | Timeout of int * t Terms.bag
     type bag = t Terms.bag * int
     val empty_state : state
+    val size_of_state : state -> int * int
     val bag_of_state :state -> bag
     val replace_bag : state -> bag -> state
     (* we suppose input has been already saturated *)

diff --git a/matitaB/components/ng_paramodulation/stats.ml b/matitaB/components/ng_paramodulation/stats.ml
index fd68f0fe765cd7cd75be5805dac8c516a0f623fb..29db6c902c6ced25c9b0f80a16d2438676c30f58 100644 (file)
--- a/matitaB/components/ng_paramodulation/stats.ml
+++ b/matitaB/components/ng_paramodulation/stats.ml
@@ -73,7 +73,7 @@ module Stats (B : Terms.Blob) =
       in 
         aux [] 
           (match goal with
-          | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
+          | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ]
          | _,Terms.Predicate p,_,_ -> p)
     ;;
 

diff --git a/matitaB/components/ng_paramodulation/superposition.ml b/matitaB/components/ng_paramodulation/superposition.ml
index 42cf063b64f08b3e352693d7a30bebff78025e95..1152571cedb3e9c5d409f9da6fa6665555c22d54 100644 (file)
--- a/matitaB/components/ng_paramodulation/superposition.ml
+++ b/matitaB/components/ng_paramodulation/superposition.ml
@@ -27,7 +27,8 @@ module Superposition (B : Orderings.Blob) =
       * B.t Terms.substitution
 
     let print s = prerr_endline (Lazy.force s);; 
-    let debug _ = ();; 
+    let debug _ = ();;
+    (* let debug = print;; *) 
     let enable = true;;
 
     let rec list_first f = function
@@ -140,7 +141,7 @@ module Superposition (B : Orderings.Blob) =
       if filter subst then
         let literal = 
           match t with
-          | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
+          | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq (B.eqP()) eq ->
                let o = Order.compare_terms l r in
                Terms.Equation (l, r, ty, o)
           | t -> Terms.Predicate t
@@ -281,12 +282,12 @@ module Superposition (B : Orderings.Blob) =
       | Terms.Equation (l,r,ty,_) ->
           let bag,l,id1 = 
            visit bag [2]
-            (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id l
+            (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ]) id l
             (ctx_demod table vl)
          in 
          let bag,_,id2 = 
             visit bag [3]
-              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 r
+              (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ]) id1 r
               (ctx_demod table vl)
          in 
           let cl,_,_ = Terms.get_from_bag id2 bag in
@@ -310,7 +311,7 @@ module Superposition (B : Orderings.Blob) =
         match lit with
           | Terms.Predicate _ -> assert false
           | Terms.Equation (l,r,ty,_) ->
-              Terms.Node [Terms.Leaf B.eqP; ty; l ; r]
+              Terms.Node [Terms.Leaf (B.eqP()); ty; l ; r]
       in
         try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true
         with FoUnif.UnificationFailure _ -> false
@@ -379,11 +380,11 @@ module Superposition (B : Orderings.Blob) =
         let reverse = (dir = Terms.Left2Right) = b in
         let l, r, proof_rewrite_dir = if reverse then l,r,Terms.Left2Right
         else r,l, Terms.Right2Left in
-          (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl)
+          (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ], vl)
       in
       let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in
       let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in
-      let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in
+      let t = Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ] in
       let locked_vars = if unify then [] else vl in
       let rec aux = function
         | [] -> None
@@ -403,7 +404,7 @@ module Superposition (B : Orderings.Blob) =
           match rewrite_eq ~unify l r ty vl table with
             | None -> None
             | Some (id2, dir, subst) ->
-                let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in
+                let id_t = Terms.Node [ Terms.Leaf (B.eqP()); ty; r; r ] in
                   build_new_clause bag maxvar (fun _ -> true)
                   Terms.Superposition id_t subst id id2 [2] dir 
     ;;
@@ -437,7 +438,7 @@ module Superposition (B : Orderings.Blob) =
                   let newsubst = Subst.concat subst1 subst in
                   let id_t = 
                     FoSubst.apply_subst newsubst
-                      (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r]) 
+                      (Terms.Node[Terms.Leaf (B.eqP());ty;contextl r;contextr r]) 
                   in
                     (match 
                       build_new_clause_reloc bag maxvar (fun _ -> true)
@@ -714,14 +715,14 @@ module Superposition (B : Orderings.Blob) =
           fold_build_new_clause bag maxvar id Terms.Superposition
             (fun _ -> true)
             (all_positions [3] 
-              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+              (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ])
               r (superposition table vl))
       | Terms.Equation (l,r,ty,Terms.Invertible)
       | Terms.Equation (l,r,ty,Terms.Gt) ->
           fold_build_new_clause bag maxvar id Terms.Superposition
             (fun _ -> true)
             (all_positions [2] 
-              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+              (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ])
               l (superposition table vl))
       | Terms.Equation (l,r,ty,Terms.Incomparable) ->
          let filtering avoid subst = (* Riazanov: p.33 condition (iv) *)
@@ -734,14 +735,14 @@ module Superposition (B : Orderings.Blob) =
            fold_build_new_clause bag maxvar id Terms.Superposition
               (filtering Terms.Gt)
               (all_positions [3] 
-                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+                (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ])
                 r (superposition table vl))
          in
          let bag, maxvar, l_terms =
            fold_build_new_clause bag maxvar id Terms.Superposition
               (filtering Terms.Lt)
               (all_positions [2] 
-                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+                (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ])
                 l (superposition table vl))
          in
            bag, maxvar, r_terms @ l_terms

diff --git a/matitaB/components/ng_paramodulation/terms.ml b/matitaB/components/ng_paramodulation/terms.ml
index e0fcad181d199f8d143373215b35fab67a2bf98e..6ad494965367a081249e0bc4d692bae70b016e0e 100644 (file)
--- a/matitaB/components/ng_paramodulation/terms.ml
+++ b/matitaB/components/ng_paramodulation/terms.ml
@@ -95,7 +95,7 @@ module type Blob =
     type t
     val eq : t -> t -> bool
     val compare : t -> t -> int
-    val eqP : t
+    val eqP : unit -> t
     val is_eq: t foterm -> (t foterm* t foterm *t foterm) option 
     val pp : t -> string
     type input

diff --git a/matitaB/components/ng_paramodulation/terms.mli b/matitaB/components/ng_paramodulation/terms.mli
index 020eefecdb74e58fc63ed4d5c96f157c6403febc..d84f37b020acdf1b2f490324d5618bea1c48bea3 100644 (file)
--- a/matitaB/components/ng_paramodulation/terms.mli
+++ b/matitaB/components/ng_paramodulation/terms.mli
@@ -83,7 +83,7 @@ module type Blob =
     type t
     val eq : t -> t -> bool
     val compare : t -> t -> int
-    val eqP : t
+    val eqP : unit -> t
     (* TODO: consider taking in input an imperative buffer for Format 
      *  val pp : Format.formatter -> t -> unit
      * *)

diff --git a/matitaB/components/ng_tactics/nTacStatus.ml b/matitaB/components/ng_tactics/nTacStatus.ml
index 3684c051f5913ea8adc9c4eca53272a2113b9b2e..3a07acc05a641de942ae1c88a2e507234d1a8384 100644 (file)
--- a/matitaB/components/ng_tactics/nTacStatus.ml
+++ b/matitaB/components/ng_tactics/nTacStatus.ml
@@ -500,6 +500,8 @@ type 'status tactic = #tac_status as 'status -> 'status
 
 let pp_tac_status (status: #tac_status) = 
   prerr_endline (status#ppobj status#obj);
+  (* let a,p = NCicParamod.size_of_state status#eq_cache in
+  prerr_endline ("number of actives: " ^ string_of_int a ^ "and number of passives: " ^ string_of_int p) *)
   prerr_endline ("STACK:\n" ^ Continuationals.Stack.pp status#stack)
 ;;
 

diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html
index 14027f7f2670ba5ff1eae7b58a1c9ad8bad18eb0..c7be10ff1a57269735d38468991692c22ed15621 100644 (file)
--- a/matitaB/matita/index.html
+++ b/matitaB/matita/index.html
@@ -24,6 +24,8 @@
           <A href="javascript:retract()"><IMG class="topimg" src="icons/retract.png" 
                                               id="retract" alt="Retract"
                                                title="Undo execution of one step of the script."></A>
+          <A href="javascript:gotoTop()"><IMG class="topimg" src="icons/top.png" 
+                                                 id="top" alt="Top" title="Undo execution of the whole script."></A>
           <A href="javascript:gotoPos()"><IMG class="topimg" src="icons/position.png" 
                                                id="cursor" alt="Play"
                                                title="Execute the script until the current position of the cursor."></A>

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 06b465b13687243cd726888c238c8353069128b8..e9e03b0b2098b7da22d0f464a668632bb111dba3 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -107,12 +107,11 @@ let output_status s =
     "<meta number=\"" ^ (string_of_int metano) ^ "\">" ^ markup ^
     txt0 ^ "</meta>" ^ acc
   in
-  let res = "<metasenv>" ^
+  "<metasenv>" ^
     (Stack.fold 
       ~env:(render_sequent true) ~cont:(render_sequent false) 
       ~todo:(render_sequent false) "" s#stack) ^
     "</metasenv>"
-  in 
   (* prerr_endline ("sending metasenv:\n" ^ res); res *)
 ;;
 
@@ -508,6 +507,41 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work() 
 ;;
 
+let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+  let env = cgi#environment in
+  prerr_endline "executing goto Top";
+  (try 
+    let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+    let sid = HExtlib.unopt sid in
+    (*
+    cgi # set_header 
+      ~cache:`No_cache 
+      ~content_type:"text/xml; charset=\"utf-8\""
+      ();
+    *)
+    let status = MatitaAuthentication.get_status sid in
+    let uid = MatitaAuthentication.user_of_session sid in
+    let baseuri = status#baseuri in
+    let new_status = new MatitaEngine.status (Some uid) baseuri in
+    NCicLibrary.time_travel new_status;
+    let new_history = [new_status] in 
+    MatitaAuthentication.set_history sid new_history;
+    MatitaAuthentication.set_status sid new_status;
+    NCicLibrary.time_travel new_status;
+    cgi # set_header 
+      ~cache:`No_cache 
+      ~content_type:"text/xml; charset=\"utf-8\""
+      ();
+    cgi#out_channel#output_string "<response>ok</response>"
+   with _ -> 
+     (cgi#set_header ~status:`Internal_server_error 
+      ~cache:`No_cache 
+      ~content_type:"text/xml; charset=\"utf-8\"" ();
+      cgi#out_channel#output_string "<response>ok</response>");
+  cgi#out_channel#commit_work()) 
+;;
+
 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   let env = cgi#environment in
@@ -644,6 +678,13 @@ let start() =
       dyn_translator = (fun _ -> ""); (* not needed *)
       dyn_accept_all_conditionals = false;
     } in
+  let goto_top =
+    { Nethttpd_services.dyn_handler = (fun _ -> gotoTop);
+      dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
+      dyn_uri = None;                 (* not needed *)
+      dyn_translator = (fun _ -> ""); (* not needed *)
+      dyn_accept_all_conditionals = false;
+    } in
   let retrieve =
     { Nethttpd_services.dyn_handler = (fun _ -> retrieve);
       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
@@ -706,6 +747,7 @@ let start() =
       ~handlers:[ "advance", do_advance
                 ; "retract", do_retract
                 ; "bottom", goto_bottom
+                ; "top", goto_top
                 ; "open", retrieve 
                 ; "register", do_register
                 ; "login", do_login 

diff --git a/matitaB/matita/matitaweb.css b/matitaB/matita/matitaweb.css
index b75aaf301cd9f7f514d54d0d54484b91d7a35c1e..aed752a8e9cde90fb5d41c1b79b6cc56684dc45b 100644 (file)
--- a/matitaB/matita/matitaweb.css
+++ b/matitaB/matita/matitaweb.css
@@ -112,7 +112,7 @@ div.navibar {
        margin-left: auto;
        margin-right: auto;
        height:100%; 
-       width:33%; 
+       width:370px; 
        float:left; 
 }
 
@@ -121,7 +121,7 @@ div.toolbar {
        margin-left: auto;
        margin-right: auto;
        height:100%; 
-       width:33%;
+       width:300px;
         float:left; 
 }
 
@@ -130,7 +130,7 @@ div.caption {
        margin-left: auto;
        margin-right: auto;
        height:100%; 
-       width:34%; 
+       width:220px; 
        text-align: center;
         float:right; 
 }

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 837c687cb9385dc22af1948d924a041deb6b997e..d9bd38aa80e94dac072b197f10cb86b1d0555032 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -535,6 +535,27 @@ function gotoBottom()
 }
 
 
+function gotoTop()
+{
+       processor = function(xml) {
+               if (is_defined(xml)) {
+                 if (xml.childNodes[0].textContent != "ok") {
+                     debug("goto top failed");
+                  }
+                  else
+                     unlocked.innerHTML = locked.innerHTML + unlocked.innerHTML
+                     locked.innerHTML = ""
+                     hideSequent();
+                     unlocked.scrollIntoView(true);
+               } else {
+                       debug("goto top failed");
+               } 
+                resume();
+       };
+       pause();
+       callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
+  
+}
 function gotoPos(offset)
 {
         if (!is_defined(offset)) {

diff --git a/matitaB/matita/netplex.conf b/matitaB/matita/netplex.conf
index 10e9c55dcfbe0a6a94419133bc45255fb0187707..858ea6e8e85c199d6badfd067f90f9e0369e507f 100644 (file)
--- a/matitaB/matita/netplex.conf
+++ b/matitaB/matita/netplex.conf
@@ -60,6 +60,13 @@ netplex {
             handler = "bottom";
           }
         };
+        uri {
+          path = "/top";
+          service {
+            type = "dynamic";
+            handler = "top";
+          }
+        };
         uri {
           path = "/register";
           service {