/[mojave]/metaprl/editor/ml/shell.ml
ViewVC logotype

Diff of /metaprl/editor/ml/shell.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 2921 by jyh, Thu Feb 24 06:55:47 2000 UTC revision 2922 by lolorigo, Thu Mar 16 19:52:02 2000 UTC
# Line 718  Line 718 
718           print_exn info create name           print_exn info create name
719    
720     let create_tptp info name =     let create_tptp info name =
721        let create name =      ()
722    (*      let create name =
723           let seq = Tptp_load.load name in           let seq = Tptp_load.load name in
724           let parse_arg = get_parse_arg info in           let parse_arg = get_parse_arg info in
725           let display_mode = get_display_mode info in           let display_mode = get_display_mode info in
# Line 729  Line 730 
730              touch info              touch info
731        in        in
732           print_exn info create name           print_exn info create name
733    *)
734     let create_opname info name =     let create_opname info name =
735        let create name =        let create name =
736           touch info;           touch info;

Legend:
Removed from v.2921  
changed lines
  Added in v.2922

  ViewVC Help
Powered by ViewVC 1.1.26