X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Ftoplevel%2Fhelena.ml;h=10c9f0f7f148d09c62f00fefc0cc1123f4b1454f;hb=9bdda2beaa7b0f836e3700a2e2458761e8eee06d;hp=1070dd9150748ca75c6456112ace31b3cd46d558;hpb=88977b2d546e547e23b046792fe2ad8f6ff192a4;p=helm.git

diff --git a/helm/software/helena/src/toplevel/helena.ml b/helm/software/helena/src/toplevel/helena.ml
index 1070dd915..10c9f0f7f 100644
--- a/helm/software/helena/src/toplevel/helena.ml
+++ b/helm/software/helena/src/toplevel/helena.ml
@@ -40,7 +40,7 @@ module BU = BrgUntrusted
 module BM = BrgMatita
 module BQ = BrgCoq
 module BH = BrgHelena
-(* module BC = BrgCC *)
+module BP = BrgPTS
 module BY = BrgLYP
 module ZD = BagCrg
 module ZO = BagOutput
@@ -386,16 +386,14 @@ END
 
 IFDEF MANAGER THEN
 
-let set_manager s = match KS.lowercase s with
+let set_manager s = match KS.lowercase_ascii s with
    | "v8"  -> G.manager := G.Coq
    | "ma2" -> G.manager := G.Matita
    | "lp1" -> G.manager := G.LP1
    | "lp2" -> G.manager := G.LP2
    | "tj2" -> G.manager := G.TJ2
    | "tj3" -> G.manager := G.TJ3
-(*
-   | "cc0" -> G.manager := G.CC0
-*)
+   | "pts" -> G.manager := G.PTS
    | "lyp" -> G.manager := G.LYP
    | s     -> L.warn level (KP.sprintf "Unknown manager: %s" s)
 
@@ -492,9 +490,7 @@ IFDEF MANAGER THEN
          | G.LP2    -> st := {!st with mst = Some (BH.open_out_lp2 base_name)}
          | G.TJ2    -> st := {!st with mst = Some (BH.open_out_tj2 base_name)}
          | G.TJ3    -> st := {!st with mst = Some (BH.open_out_tj3 base_name)}
-(*
-         | G.CC0    -> st := {!st with mst = Some (BC.open_out_cc0 base_name)}
-*)
+         | G.PTS    -> st := {!st with mst = Some (BP.open_out_pts2 base_name)}
          | G.LYP    -> st := {!st with mst = Some (BY.open_out_lyp2 base_name)}
          | G.Quiet  -> ()
       end
@@ -530,7 +526,7 @@ ELSE () END
       "              4 typing information, 5 conversion information, 6 reduction information,\n" ^
       "              7 level disambiguation\n\n" ^
       "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n\n" ^
-      "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"lp1\" \"lp2\" \"tj2\" \"tj3\" \"lyp\" (lambda-Prolog)\n" 
+      "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"lp1\" \"lp2\" \"tj2\" \"tj3\" \"pts\" \"lyp\" (lambda-Prolog)\n" 
    in
    let help_L = "         [lexer]     Show lexer debug information" in 
    let help_M = "<dir>    [manager]   Set location of output directory (manager) to <dir> (default: current directory)" in