equal
deleted
inserted
replaced
111 must be be replaced by the given pattern. However, we have to remove all |
111 must be be replaced by the given pattern. However, we have to remove all |
112 ellipses from it and replace them by @{text [quotes] "_"}. The following |
112 ellipses from it and replace them by @{text [quotes] "_"}. The following |
113 function will do this: |
113 function will do this: |
114 *} |
114 *} |
115 |
115 |
116 ML{*fun ml_pat (code_txt, pat) = |
116 ML %grayML{*fun ml_pat (code_txt, pat) = |
117 let val pat' = |
117 let val pat' = |
118 implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
118 implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
119 in |
119 in |
120 "val " ^ pat' ^ " = " ^ code_txt |
120 "val " ^ pat' ^ " = " ^ code_txt |
121 end*} |
121 end*} |
123 text {* |
123 text {* |
124 Next we add a response indicator to the result using: |
124 Next we add a response indicator to the result using: |
125 *} |
125 *} |
126 |
126 |
127 |
127 |
128 ML{*fun add_resp pat = map (fn s => "> " ^ s) pat*} |
128 ML %grayML{*fun add_resp pat = map (fn s => "> " ^ s) pat*} |
129 |
129 |
130 text {* |
130 text {* |
131 The rest of the code of @{text "ML_resp"} is: |
131 The rest of the code of @{text "ML_resp"} is: |
132 *} |
132 *} |
133 |
133 |