Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/ML/ml_process.scala
changeset 72614 ffed574c65c3
parent 72613 d01ea9e3bd2d
child 72615 f827c3bb6b7f 
--- a/src/Pure/ML/ml_process.scala	Sun Nov 15 17:34:19 2020 +0100
+++ b/src/Pure/ML/ml_process.scala	Sun Nov 15 17:42:35 2020 +0100
@@ -86,15 +86,15 @@
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
                 ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
-          def print_list(list: List[String]): String =
-            ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
-          def print_sessions(list: List[(String, Position.T)]): String =
+          def print_list: List[String] => String =
+            ML_Syntax.print_list(ML_Syntax.print_string_bytes)
+          def print_sessions: List[(String, Position.T)] => String =
             ML_Syntax.print_list(
-              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
-          def print_bibtex_entries(list: List[(String, List[String])]): String =
+              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))
+          def print_bibtex_entries: List[(String, List[String])] => String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(ML_Syntax.print_string_bytes,
-                ML_Syntax.print_list(ML_Syntax.print_string_bytes)))(list)
+                ML_Syntax.print_list(ML_Syntax.print_string_bytes)))
 
           List("Resources.init_session" +
             "{session_positions = " + print_sessions(sessions_structure.session_positions) +
isabelle