Definitions EditorDoc Sections Nuprl Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
No other cites to report in EditorDoc
scan_lib_fileDef MLmacro
Def ScanLibFile: FileName
Def AtFirst atfirst Eof ifeof WithNextifnoteof

Def help
Def == let fname  complete_file_name FileName in
Def == {Open the file then apply the function to Eof predicate and a Next
Def == {operator, which returns the first entry, then advances the file. }
Def == new_load_file fname
Def == (Eof.Next.
Def == (letrec ScanRest SoFar
Def == (letrec  if Eof () then ifeof else
Def == (letrec  let fobtok,fobkind,fobterm,fobruletree,fobload  Next () ,
Def == (letrec  let fobload tk
Def == (letrec  let  fobload tk ;
Def == (letrec  let  (if fobkind=`THM` thendo complete_thm_load tk) ,
Def == (letrec  let fobstr  tok_to_string fobtok ,
Def == (letrec  let tagterm ()
Def == (letrec  let  plug_enum
Def == (letrec  let  #COVER 
Def == (letrec  let  1 2 from 4  3 : term
Def == (letrec  let  #
Def == (letrec  let  IMP:IMPLODE
Def == (letrec  let  IMP:Icomment{pre:s}(
Def == (letrec  let  IMP:IcommentIMPLODE variable{3:v}; IMPLODE
Def == (letrec  let  IMP:IcommentIMPLODE variable{3:v}; Ivariable{1:v}
Def == (letrec  let  IMP:IcommentIMPLODE variable{2:v} from IMPLODE
Def == (letrec  let  IMP:IcommentIMPLODE variable{2:v} from Ivariable{4:v}) 
Def == (letrec  let  [tok_to_word fobkind
Def == (letrec  let  ;make_obref fobtok
Def == (letrec  let  ;fobterm
Def == (letrec  let  ;string_to_word fname] in
Def == (letrec  ifnoteof in
Def == (ScanRest atfirst)
ml_implode_termDef MLmacro
Def IMP:T  == edit_implode_all T
ml_applyDef ml, ml_apply
Def a b == ((a)(b))
ml_nilDef ml
Def [] == []
ml_consDef ml, ml_cons
Def a.b == ((a).(b))
ml_doifDef ml
Def if a thendo b == if a then do b else ()
ml_theunitDef ml
Def () == ()
ml_letinDef ml, ml_let, nospaces
Def let$mod a  b in c == let$mod a  b in c
ml_tokDef ml, possible_ob_ref
Def `$tok` == `$tok`
ml_eqDef ml, ml_eq
Def a=b == ((a)=(b))
ml_seqDef ml, ml_seq
Def a ; b == ((a);(b))
ml_pairDef ml
Def a,b == ((a),(b))
ml_ifDef ml
Def if a then b else c == if a then b else c
ml_lambdaDef ml, NoConds
Def a.b == (\a.(b))
ml_declDef ml
Def a  b == a=(b)
ml_letin_wrapDef ml, nospaces
Def let$mod D in c == let$mod D in (c)
ml_do_unopDef ml
Def do X == (do (X))
ml_testDef ml
Def if a $then b $else c == if (a) $then (b) $else c
ml_parensDef ml, slots_not_slots
Def (a) == (a)
ml_tokoDef ml, semi_puretext
Def `s` == `s`

Syntax:ScanLibFile: FileName
AtFirst atfirst Eof ifeof WithNextifnoteof

help
has structure: scan_lib_file(FileNameifeofifnoteofatfirsthelp)

About:
!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions EditorDoc Sections Nuprl Doc