summaryrefslogtreecommitdiff
path: root/contrib/extraction/test/make_mli
blob: 40ee496ea244253d1a015a97f38d2027711ec917 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
#!/usr/bin/awk -We $0

{ match($0,"^open") 
  if (RLENGTH>0) state=1
  match($0,"^type") 
  if (RLENGTH>0) state=1 
  match($0,"^\(\*\* ")
  if (RLENGTH>0) state=2
  match($0,"^let")
  if (RLENGTH>0) state=0
  match($0,"^and")
  if ((RLENGTH>0) && (state==2)) state=0
  if ((RLENGTH>0) && (state==1)) state=1		     
  gsub("\(\*\* ","")
  gsub("\*\*\)","")
  if (state>0) print
}