src/Pure/ML/ml_process.scala
changeset 72854 5fc193537b7c
parent 72853 217e6cf61453
child 72859 429afd0d1a79
equal deleted inserted replaced
72853:217e6cf61453 72854:5fc193537b7c
    83     Isabelle_System.chmod("600", File.path(init_session))
    83     Isabelle_System.chmod("600", File.path(init_session))
    84     File.write(init_session,
    84     File.write(init_session,
    85       session_base match {
    85       session_base match {
    86         case None => ""
    86         case None => ""
    87         case Some(base) =>
    87         case Some(base) =>
    88           def print_table(table: List[(String, String)]): String =
    88           def print_table: List[(String, String)] => String =
    89             ML_Syntax.print_list(
    89             ML_Syntax.print_list(
    90               ML_Syntax.print_pair(
    90               ML_Syntax.print_pair(
    91                 ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
    91                 ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))
    92           def print_list: List[String] => String =
    92           def print_list: List[String] => String =
    93             ML_Syntax.print_list(ML_Syntax.print_string_bytes)
    93             ML_Syntax.print_list(ML_Syntax.print_string_bytes)
    94           def print_sessions: List[(String, Position.T)] => String =
    94           def print_sessions: List[(String, Position.T)] => String =
    95             ML_Syntax.print_list(
    95             ML_Syntax.print_list(
    96               ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))
    96               ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))