*** empty log message ***

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index a3e369057eea263c1522069e422297062efbe924..4363b3beee623f7e22db32dd5658746c8b89859c 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -27,7 +27,7 @@
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
 (*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                Claudio Sacerdoti Coen <natile@cs.unibo.it>               *)
 (*                                 06/01/2002                                 *)
 (*                                                                            *)
 (*                                                                            *)
@@ -60,12 +60,12 @@ let htmlfooter =
  "</html>"
 ;;
 
-let prooffile = "/public/sacerdot/currentproof";;
-let prooffiletype = "/public/sacerdot/currentprooftype";;
+let prooffile = "/public/natile/currentproof";;
+let prooffiletype = "/public/natile/currentprooftype";;
 
 (* SACERDOT
-let prooffile = "/public/sacerdot/currentproof";;
-let prooffiletype = "/public/sacerdot/currentprooftype";;
+let prooffile = "/public/natile/currentproof";;
+let prooffiletype = "/public/natile/currentprooftype";;
 *)
 
 (* TASSI
@@ -80,12 +80,12 @@ let prooffiletype = "/home/galata/miohelm/currentprooftype";;
 
 (*CSC: the getter should handle the innertypes, not the FS *)
 
-let innertypesfile = "/public/sacerdot/innertypes";;
-let constanttypefile = "/public/sacerdot/constanttype";;
+let innertypesfile = "/public/natile/innertypes";;
+let constanttypefile = "/public/natile/constanttype";;
 
 (* SACERDOT
-let innertypesfile = "/public/sacerdot/innertypes";;
-let constanttypefile = "/public/sacerdot/constanttype";;
+let innertypesfile = "/public/natile/innertypes";;
+let constanttypefile = "/public/natile/constanttype";;
 *)
 
 (* TASSI
@@ -2369,7 +2369,10 @@ let completeSearchPattern () =
   try
    let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in
    let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in
-    ignore (MQueryLevels2.get_constraints expr)
+   let must,can = MQueryLevels2.get_constraints expr in
+   let result = MQueryGenerator.searchPattern must can in 
+    output_html outputhtml
+     ("<h1 color=\"maroon\"><pre>" ^ MQueryUtil.text_of_result result "\n" ^ "</pre></h1>")
   with
    e ->
     output_html outputhtml
@@ -2516,7 +2519,14 @@ let searchPattern () =
          let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
           let list_of_must,can = MQueryLevels.out_restr metasenv ey ty in
          let must = choose_must list_of_must can in
-         let result = MQueryGenerator.searchPattern metasenv ey ty must can in
+         let torigth_restriction (u,b) =
+            let p = if b then "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" 
+                    else "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" in
+              (u,p,None)
+         in
+         let rigth_must = List.map torigth_restriction must in
+         let rigth_can = Some (List.map torigth_restriction can) in
+         let result = MQueryGenerator.searchPattern (rigth_must,[],[]) (rigth_can,None,None) in 
           let uris =
            List.map
             (function uri,_ ->