lib/scripts/feeder.pl
author wenzelm
Wed, 19 Jan 2011 21:45:50 +0100
changeset 41616 aa002926cbf1
parent 40335 3e4bb6e7c3ca
child 47868 32c03d45fffe
permissions -rw-r--r--
potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     1
#
9789
wenzelm
parents: 6281
diff changeset
     2
# Author: Markus Wenzel, TU Muenchen
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     3
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     4
# feeder.pl - feed isabelle session
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     5
#
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     6
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     7
# args
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
     8
12111
d942348d8faf got rid of obsolete input filtering;
wenzelm
parents: 9961
diff changeset
     9
($head, $emitpid, $quit, $tail) = @ARGV;
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    10
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    11
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    12
# setup signal handlers
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    13
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    14
sub hangup { exit(0); }
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    15
$SIG{'HUP'} = "hangup";
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    16
$SIG{'INT'} = "IGNORE";
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    17
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    18
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    19
# main
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    20
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    21
#buffer lines
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    22
$| = 1;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    23
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    24
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    25
$emitpid && (print $$, "\n");
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    26
40335
3e4bb6e7c3ca feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
wenzelm
parents: 39580
diff changeset
    27
if ($head) {
41616
aa002926cbf1 potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);
wenzelm
parents: 40335
diff changeset
    28
  utf8::upgrade($head);
40335
3e4bb6e7c3ca feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
wenzelm
parents: 39580
diff changeset
    29
  $head =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
3e4bb6e7c3ca feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
wenzelm
parents: 39580
diff changeset
    30
  print $head, "\n";
3e4bb6e7c3ca feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
wenzelm
parents: 39580
diff changeset
    31
}
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    32
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    33
if (!$quit) {
39580
05daab5782f6 tuned whitespace;
wenzelm
parents: 29145
diff changeset
    34
  while (<STDIN>) {
05daab5782f6 tuned whitespace;
wenzelm
parents: 29145
diff changeset
    35
    print;
05daab5782f6 tuned whitespace;
wenzelm
parents: 29145
diff changeset
    36
  }
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    37
}
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    38
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    39
$tail && (print "$tail", "\n");
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    40
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    41
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    42
# wait forever
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    43
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    44
close STDOUT;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    45
sleep;