src/Pure/Tools/isabelle_process.ML
changeset 27972 a87be8fcb25c
parent 27961 2cd133df7587
child 27986 26e1a7a6695d
equal deleted inserted replaced
27971:57dc3bd6f841 27972:a87be8fcb25c
    56   let val clean = clean_string [Symbol.STX, "\n", "\r"]
    56   let val clean = clean_string [Symbol.STX, "\n", "\r"]
    57   in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
    57   in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
    58 
    58 
    59 fun message_text class ts =
    59 fun message_text class ts =
    60   let
    60   let
    61     val doc = XML.Elem ("message", [("class", class)], ts);
    61     val doc = XML.Elem (Markup.messageN, [(Markup.classN, class)], ts);
    62     val msg =
    62     val msg =
    63       if print_mode_active xmlN then XML.header ^ XML.string_of doc
    63       if print_mode_active xmlN then XML.header ^ XML.string_of doc
    64       else YXML.string_of doc;
    64       else YXML.string_of doc;
    65   in clean_string [Symbol.STX] msg end;
    65   in clean_string [Symbol.STX] msg end;
    66 
    66 
    83           |> Position.default_properties pos;
    83           |> Position.default_properties pos;
    84       in Output.writeln_default (special ch ^ message_props props ^ txt ^ special_end) end;
    84       in Output.writeln_default (special ch ^ message_props props ^ txt ^ special_end) end;
    85 
    85 
    86 fun init_message () =
    86 fun init_message () =
    87   let
    87   let
    88     val pid = ("pid", string_of_pid (Posix.ProcEnv.getpid ()));
    88     val class = (Markup.classN, Markup.initN);
    89     val session = ("session", List.last (Session.id ()) handle List.Empty => "unknown");
    89     val pid = (Markup.pidN, string_of_pid (Posix.ProcEnv.getpid ()));
    90     val welcome = Session.welcome ();
    90     val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
    91   in Output.writeln_default (special "H" ^ message_props [pid, session] ^ welcome ^ special_end) end;
    91     val props = message_props [class, pid, session];
       
    92   in Output.writeln_default (special "H" ^ props ^ Session.welcome () ^ special_end) end;
    92 
    93 
    93 end;
    94 end;
    94 
    95 
    95 
    96 
    96 (* channels *)
    97 (* channels *)
    97 
    98 
    98 fun setup_channels () =
    99 fun setup_channels () =
    99  (Output.writeln_fn  := message "A" "writeln";
   100  (Output.writeln_fn  := message "A" Markup.writelnN;
   100   Output.priority_fn := message "B" "priority";
   101   Output.priority_fn := message "B" Markup.priorityN;
   101   Output.tracing_fn  := message "C" "tracing";
   102   Output.tracing_fn  := message "C" Markup.tracingN;
   102   Output.warning_fn  := message "D" "warning";
   103   Output.warning_fn  := message "D" Markup.warningN;
   103   Output.error_fn    := message "E" "error";
   104   Output.error_fn    := message "E" Markup.errorN;
   104   Output.debug_fn    := message "F" "debug";
   105   Output.debug_fn    := message "F" Markup.debugN;
   105   Output.prompt_fn   := message "G" "prompt";
   106   Output.prompt_fn   := message "G" Markup.promptN;
   106   Output.status_fn   := message "I" "status");
   107   Output.status_fn   := message "I" Markup.statusN);
   107 
   108 
   108 
   109 
   109 (* init *)
   110 (* init *)
   110 
   111 
   111 fun init () =
   112 fun init () =
   113   setup_channels ();
   114   setup_channels ();
   114   init_message ();
   115   init_message ();
   115   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
   116   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
   116 
   117 
   117 end;
   118 end;
   118