equal
deleted
inserted
replaced
118 val path = Path.explode s; |
118 val path = Path.explode s; |
119 val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path)); |
119 val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path)); |
120 in () end))); |
120 in () end))); |
121 \<close> |
121 \<close> |
122 |
122 |
123 external_file "$POLYML_EXE" |
|
124 |
|
125 |
123 |
126 subsection \<open>Embedded ML text\<close> |
124 subsection \<open>Embedded ML text\<close> |
127 |
125 |
128 ML \<open> |
126 ML \<open> |
129 local |
127 local |