symbolic message markup;
authorwenzelm
Sat Aug 23 23:07:43 2008 +0200 (2008-08-23)
changeset 27972a87be8fcb25c
parent 27971 57dc3bd6f841
child 27973 18d02c0b90b6
symbolic message markup;
init message: class property;
src/Pure/Tools/isabelle_process.ML
     1.1 --- a/src/Pure/Tools/isabelle_process.ML	Sat Aug 23 23:07:41 2008 +0200
     1.2 +++ b/src/Pure/Tools/isabelle_process.ML	Sat Aug 23 23:07:43 2008 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4  
     1.5  fun message_text class ts =
     1.6    let
     1.7 -    val doc = XML.Elem ("message", [("class", class)], ts);
     1.8 +    val doc = XML.Elem (Markup.messageN, [(Markup.classN, class)], ts);
     1.9      val msg =
    1.10        if print_mode_active xmlN then XML.header ^ XML.string_of doc
    1.11        else YXML.string_of doc;
    1.12 @@ -85,10 +85,11 @@
    1.13  
    1.14  fun init_message () =
    1.15    let
    1.16 -    val pid = ("pid", string_of_pid (Posix.ProcEnv.getpid ()));
    1.17 -    val session = ("session", List.last (Session.id ()) handle List.Empty => "unknown");
    1.18 -    val welcome = Session.welcome ();
    1.19 -  in Output.writeln_default (special "H" ^ message_props [pid, session] ^ welcome ^ special_end) end;
    1.20 +    val class = (Markup.classN, Markup.initN);
    1.21 +    val pid = (Markup.pidN, string_of_pid (Posix.ProcEnv.getpid ()));
    1.22 +    val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
    1.23 +    val props = message_props [class, pid, session];
    1.24 +  in Output.writeln_default (special "H" ^ props ^ Session.welcome () ^ special_end) end;
    1.25  
    1.26  end;
    1.27  
    1.28 @@ -96,14 +97,14 @@
    1.29  (* channels *)
    1.30  
    1.31  fun setup_channels () =
    1.32 - (Output.writeln_fn  := message "A" "writeln";
    1.33 -  Output.priority_fn := message "B" "priority";
    1.34 -  Output.tracing_fn  := message "C" "tracing";
    1.35 -  Output.warning_fn  := message "D" "warning";
    1.36 -  Output.error_fn    := message "E" "error";
    1.37 -  Output.debug_fn    := message "F" "debug";
    1.38 -  Output.prompt_fn   := message "G" "prompt";
    1.39 -  Output.status_fn   := message "I" "status");
    1.40 + (Output.writeln_fn  := message "A" Markup.writelnN;
    1.41 +  Output.priority_fn := message "B" Markup.priorityN;
    1.42 +  Output.tracing_fn  := message "C" Markup.tracingN;
    1.43 +  Output.warning_fn  := message "D" Markup.warningN;
    1.44 +  Output.error_fn    := message "E" Markup.errorN;
    1.45 +  Output.debug_fn    := message "F" Markup.debugN;
    1.46 +  Output.prompt_fn   := message "G" Markup.promptN;
    1.47 +  Output.status_fn   := message "I" Markup.statusN);
    1.48  
    1.49  
    1.50  (* init *)
    1.51 @@ -115,4 +116,3 @@
    1.52    Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
    1.53  
    1.54  end;
    1.55 -