Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/General/scan.ML
author kleing
Sat, 30 Apr 2005 14:18:36 +0200
changeset 15900 d6156cb8dc2e
parent 15664 7c150afba112
child 16002 e0557c452138
permissions -rw-r--r--
fixed typo
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11523
9a658fe20107 Tuned function extend_lexicon.
berghofe
parents: 10746
diff changeset 
     1
 
(*  Title:      Pure/General/scan.ML
9a658fe20107 Tuned function extend_lexicon.
berghofe
parents: 10746
diff changeset 
     2
 
    ID:         $Id$
9a658fe20107 Tuned function extend_lexicon.
berghofe
parents: 10746
diff changeset 
     3
 
    Author:     Markus Wenzel and Tobias Nipkow, TU Muenchen
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset 
     4
 












8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;



wenzelm


parents: 

diff
changeset




     5


Generic scanners (for potentially infinite input).













8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;



wenzelm


parents: 

diff
changeset




     6


*)













8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;



wenzelm


parents: 

diff
changeset




     7














8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;



wenzelm


parents: 

diff
changeset




     8


infix 5 -- :-- |-- --| ^^;













8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;



wenzelm


parents: 

diff
changeset




     9


infix 3 >>;













8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;



wenzelm


parents: 

diff
changeset




    10


infix 0 ||;













8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;



wenzelm


parents: 

diff
changeset




    11














8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;



wenzelm


parents: 

diff
changeset




    12


signature BASIC_SCAN =













8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;



wenzelm


parents: 

diff
changeset




    13


sig








14677






33a37f091dc5
tuned presentation;



wenzelm


parents: 
14108

diff
changeset




    14


  (*error msg handler*)








6116






8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;



wenzelm


parents: 

diff
changeset




    15


  val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b








14677