Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4); Wed, 13 Jan 1993 22:07:50 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26548;
          Wed, 13 Jan 93 13:27:11 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA26541;
          Wed, 13 Jan 93 13:27:00 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA25695;
          Wed, 13 Jan 93 13:26:27 -0800
Message-Id: <9301132126.AA25695@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list)
Subject: autoload
Date: Wed, 13 Jan 93 13:26:23 PST
From: chou@edu.ucla.cs

If I set up autoloading action for a string `abc` using the
ML function autoload(`abc`, ...) and then type, say,

# abc, abc ;;

it seems that the ML parser will execute the autoloading action
twice, once per occurrence of abc.  On the other hand, if I set
up autoloading action using autoload_theory, it seems that the
autoloading action will be executed only once no matter how many
times abc occurs.  Why is this so?

- Ching Tsun

PS. The relevant ML codes are listed below:

let autoload_term_prefix = `autoload_term_`
and autoload_type_prefix = `autoload_type_`
;;

let term_msg_lfn [thy; name] =
  ( if (get_flag_value `print_load`) then
    ( print_string (`Term `^name^` autoloaded from theory \``^thy^`\`.`) ;
      print_newline () ) ) ;
  undo_autoload name ;
  (lhs o snd o strip_forall o concl)
    (theorem thy (autoload_term_prefix^name))
;;

let autoload_term [thy; name] =
  let_before (name, `term_msg_lfn`, [thy; name])
;;

let type_msg_lfn [thy; name] =
  ( if (get_flag_value `print_load`) then
    ( print_string (`Type `^name^` autoloaded from theory \``^thy^`\`.`) ;
      print_newline () ) ) ;
  undo_autoload name ;
  (type_of o lhs o snd o strip_forall o concl)
    (theorem thy (autoload_type_prefix^name))
;;

let autoload_type [thy; name] =
  let_before (name, `type_msg_lfn`, [thy; name])
;;

let gen_autoload_theory (kind, thy, name) =
  if (mem kind [`axiom`; `definition`; `theorem`]) then
    autoload_theory (kind, thy, name)
  if (kind = `term`) then
    autoload (name, `autoload_term`, [thy; name])
  if (kind = `type`) then
    autoload (name, `autoload_type`, [thy; name])
  else
    failwith (`gen_autoload_theory: unknown kind: `^kind)
;;