lib/scripts/feeder.pl
author wenzelm
Wed, 10 Feb 2016 14:14:43 +0100
changeset 62278 c04e97be39d3
parent 61187 ff00ad5dc03a
permissions -rw-r--r--
misc tuning and updates;
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
$SIG{'INT'} = "IGNORE";
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    15
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    16
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    17
# main
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    18
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    19
#buffer lines
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    20
$| = 1;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    21
61187
ff00ad5dc03a recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents: 47868
diff changeset
    22
sub emit {
ff00ad5dc03a recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents: 47868
diff changeset
    23
  my ($text) = @_;
ff00ad5dc03a recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents: 47868
diff changeset
    24
  if ($text) {
ff00ad5dc03a recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents: 47868
diff changeset
    25
    utf8::upgrade($text);
ff00ad5dc03a recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents: 47868
diff changeset
    26
    $text =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
ff00ad5dc03a recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents: 47868
diff changeset
    27
    print $text, "\n";
ff00ad5dc03a recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents: 47868
diff changeset
    28
  }
ff00ad5dc03a recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents: 47868
diff changeset
    29
}
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    30
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    31
$emitpid && (print $$, "\n");
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    32
61187
ff00ad5dc03a recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents: 47868
diff changeset
    33
emit("$head");
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    34
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    35
if (!$quit) {
39580
05daab5782f6 tuned whitespace;
wenzelm
parents: 29145
diff changeset
    36
  while (<STDIN>) {
05daab5782f6 tuned whitespace;
wenzelm
parents: 29145
diff changeset
    37
    print;
05daab5782f6 tuned whitespace;
wenzelm
parents: 29145
diff changeset
    38
  }
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    39
}
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    40
61187
ff00ad5dc03a recode all text, which is relevant for Session.save on non-ASCII directory;
wenzelm
parents: 47868
diff changeset
    41
emit("$tail");
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    42
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    43
4504
2f39aa4bebf3 removed -i option;
wenzelm
parents: 4501
diff changeset
    44
# wait forever
4501
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    45
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    46
close STDOUT;
5f629ee2502b feed isabelle session;
wenzelm
parents:
diff changeset
    47
sleep;